Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
0
votes
1answer
45 views
D flip flop : How does it work in depth
I'm coming to you today because I have some trouble to understand how works D flip flop in depth. Two weeks ago we started at school learning sequential logic and so register and everything that come ...
5
votes
2answers
46 views
Topology vs sigma-algebra's as a framework for approximate information?
In the book "topology via logic" by Steven Vickers, topology is introduced for computer scientists, with the idea that topology captures the idea of approximate information.
I am somewhat confused ...
2
votes
2answers
83 views
Decidability of equivalence to existential formulas
I'm looking for an algorithm to recognise if a given first order formula over a fixed vocabulary admits a logically equivalent existential one (i.e. a formula in prenex form where all quantifiers are ...
0
votes
1answer
39 views
How to evaluate dynamical conditioning/pseudo code
I am having a hard time even to formulate my question, so here it is:
I have an application that the user can go in and define on a webpage the logic one wants to evaluate for the student to comply ...
1
vote
1answer
38 views
What is the signature of a formal language?
I will briefly state the context where my doubts arise.
I know the following definitions.
A formal language is a set of well-formed formulas. It's a tuple constituited by an alphabet and a formal ...
0
votes
0answers
16 views
Can I use the Quine-McCluskey to simplify a CNF which is not a product of maxterms?
As I understand it the Quine-McCluskey method allows you to start with a set of maxterms (or minterms), and combine them pairwise in a systematic way into a smaller set of clauses with a smaller set ...
0
votes
0answers
13 views
KB implication vs and
i m doing KB from sentence to model.
I m stuck on this sentence that say this :
The packages stored in room1 are smaller than those stored in room 2.
I m created this vocabulary
Package X
...
2
votes
2answers
64 views
Absorption rule in Boolean algebra
I am confused regarding the absorption rule which states: A OR (A AND B) = A.
I do not completely understand how the expression simplifies to A and while i have seen proofs for this question, i still ...
1
vote
2answers
49 views
If you can represent/model a Conditional IF statement with AND + NOT or OR + NOT
I am still trying to wrap my head around this, which shows how to simulate control-flow without using an if-statement.
I've been looking at basic logic today and ...
0
votes
2answers
50 views
How “add” could be implemented in only bitshift operations
Typically, add/subtract/multiply/divide are primitive operations in an Instruction Set Architecture (ISA). I am interested to know if they can instead be implemented efficiently using only bitshift ...
1
vote
1answer
44 views
does the order of the rows matter? [closed]
from my understanding the truth table is supposed to generate every possible combination of true and false values without the order of the combination taking into account.
however one of my teachers ...
-1
votes
0answers
126 views
Bidirectional search on permutation
Can any one tell me where I will get the source to study this topic and can able to solve the following problems?
1. (max 2 points)
Prove that for any positive integer n, the permutation (n, n − 1, . ....
0
votes
2answers
30 views
Why we treat sentence letter $Q$ as conclusion in one form and premise in other?
Sorry for asking such a dumb question.
I am CS student and I am trying to understand the basic tenets of Logic. I am new to the subject and I am lost understanding Implication.
In formal logic, $(P\...
1
vote
0answers
16 views
Superposition calculus: greater vs greater-or-equal
Bachmair and Ganzinger 1991, 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', specifies the criterion for using an equation as, by some appropriate ordering, ...
1
vote
0answers
183 views
Could you show the intractibility of SAT by showing that the number of variables contributing to an arbitrary unsatisfied clause is not constant? [closed]
Preface: This is not an attempted proof at P vs NP
Starting with some CNF Boolean expression ϕ, by the rules of logical disjunction, a clause is only unsatisfied if each of the literals in it are ...
0
votes
1answer
29 views
Can you connect an output from a logic gate to 2 or more logic gates or inputs?
I have been given this diagram of a circuit:
https://www.google.com/search?q=full+adder+logic+gate&rlz=1C1CHBF_enCA831CA831&source=lnms&tbm=isch&sa=X&ved=...
0
votes
1answer
26 views
Simplifying SOP: implementing OR with NAND
I am learning how to implement basic logic gates using NAND. I have learnt that you can use De Morgan's theorem as such:
$a+b = \bar{\bar a} + \bar{\bar b} = \overline{(\bar a *\bar b)}$
In other ...
0
votes
1answer
23 views
Superposition calculus: Elimination of redundant atoms
Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', section 5.2, 'Simplification and Deletion Techniques', page 17, 'Elimination of redundant ...
2
votes
1answer
38 views
Reasoning about resources: “resource logics”?
Are there extensions of predicate logic which focus on resource models, possibly even in actor models?
And if so, would it be possible to reason on a meta-level on how many resources should be ...
1
vote
1answer
20 views
Bachmair and Ganzinger, ordering of equations
Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', page 4, defines an order on equations. (This is an arcane piece of machinery but a critical ...
0
votes
1answer
40 views
Find value of $a$ or $b$ of two XOR equations
Is it possible to find $a$ or $b$ given that $a \oplus b = c$ and $c \oplus b = a$ when I only have the value of $b$?
0
votes
1answer
36 views
How to “logically” solve boolean logic
I came across of one excellent book Elements of Computing Systems and in chapter 1 we need to implement the "primitive" logic gates (for example: Not, And, Or, Xor, Mux, etc) based on a Nand gate.
...
1
vote
1answer
28 views
Check if one condition includes another
I have two conditions A and B in a form of "ast tree".
How can I check that B is more strict than A?
I.e. if B is true then A is always true.
Example
A:
x = 1 and (b = 2 or c = d)
B:
y = 5 and x = ...
1
vote
0answers
27 views
Why Modus ponens works with Horn clauses and Generalized Modus ponens requires definite clauses?
I am reading the Artificial Intelligence: A Modern Approach book and in the chapters about logic i noticed that in propositional logic the Modus ponens inference rule (used by the forward and backward ...
1
vote
1answer
39 views
Validity of CTL formula $s_0 \models EG\ AF\ p$ in given model
I have been learning Verification by model checking recently and I get the following question:
Is the CTL formula $s_{0} \models EG\ AF\ p$ valid in the following model?
I think it is ...
1
vote
1answer
24 views
How to prove a LTL formula correct in a specific model?
I have been learning Verification by model checking recently and I get the following question:
$Whether\ the\ LTL\ formula\ M, q_3\ \models (X\ \lnot a) \rightarrow (F\ G\ \lnot a)\ is\ established\ ...
0
votes
1answer
111 views
Can this set of propositions be represented and proved in Haskell?
I used a set of natural language statements and their formalization from Gries and Schneider. I attempted to transform the propositions into Haskell equations. For example, for S0 : $a \land w \...
3
votes
0answers
18 views
conversion of basic $\text{CTL}^*$ formulas to $\text{CTL}$
Consider the $\text{CTL}^*$ formula $E[pU(qUr)]$.
It is not hard to show that it is equivalent to the $\text{CTL}$ formula $E[pU(EqUr)]$.
The informal reason is that a path where $p$ is true until $...
1
vote
2answers
65 views
Must $x$ and $y$ be different in a statement of the form $\forall x \forall y \cdots$?
Given the following predicate formula $F$:
$$\forall x \forall y [(\text{italian}(x) \Rightarrow (\text{winWC}(y) \Rightarrow \text{happy}(x))]$$
I am having trouble understanding whether $x$ and $y$...
3
votes
1answer
64 views
Roadmap to formal verification
I would like to learn about different approaches to formal verification of software programs that goes beyond what Wikipedia has to offer. Ideally one would not only get an overview but also ...
1
vote
2answers
67 views
Validity of □(P→ Q) → (◊P → ◊Q) in linear temporal logic
How can I prove that $\Box(P\rightarrow Q)\rightarrow (\Diamond P\rightarrow\Diamond Q)$ is valid in linear temporal logic (LTL)?
0
votes
0answers
32 views
Turing machine, tape without blanks, does it halt or no?
So I'm lost on this one. We're given a turing machine and an initial tape. Tape is infinitely long in both ways, but all the blanks are taken out. The head is the leftmost nonblank. So the question is:...
0
votes
0answers
11 views
Timed Kripke structures with inequality constraints
I am having problems creating a timed Kripke structure $\mathcal{TK} = \langle S, \mathcal{T}, \rightarrow, L \rangle$ for a system that I have.
My system, a timed automaton system (time base $\...
1
vote
0answers
23 views
Unification algorithm that directly finds multiple substitutions?
Systems of formal logic generally have inference rules that
require certain expressions to be syntactically the same
in multiple steps. Typically two steps are involved, as
for modus ponens, where ...
1
vote
3answers
111 views
Soundness and completeness w.r.t. programming languages
I'm studying programming languages (more specifically type systems) and came across a concept I couldn't quite wrap my head around: soundness and completeness.
I'm taking a class, and according to my ...
0
votes
1answer
39 views
Finding CNF of $(p \rightarrow q) \rightarrow p$ and $\lnot (q \wedge (\lnot p \rightarrow q)) $
I'm trying to find the CNF of the $(p \rightarrow q) \rightarrow p$ and $\lnot (q \wedge (\lnot p \rightarrow q))$, and afterwards proving it's validity. As i'm new to CNF i wanted to ensure i've ...
1
vote
1answer
37 views
predicate logic proof of 2 numbers
For any two different numbers there is an number in between.
I'm trying to write this in predicate logic and have no idea how to do it, since I need 2 variables X and Y? For all x there exists a y ...
-1
votes
1answer
27 views
predicate logic/binary relation help
(1) ∀x, y, z (x < y ∧ y < z → x < z) (transitivity)
(2) ∀x ¬(x < x) (antisymmetry)
(3) ∀x, y (x < y ∨ x = y ∨ y < x) (linearity)
I need to give an example of a (nonempty) ...
0
votes
1answer
34 views
Would hypercomputation machines be capable of simulating/computing/programming everything?
If uncomputable numbers existed, could this hypercomputation machines compute them? Could hypercomputation compute all types of uncomputable things? Even truly inconsistent things? Even things that ...
3
votes
2answers
69 views
How could a formal system ever be non-obviously unsound?
When reading discussions of Gödel's theorems one is always heeded that just because formal system $F$ proves a theorem $T$ that doesn't necessarily mean that when one applies the intended ...
0
votes
1answer
24 views
Determining cycle time and and hold time in logic circuits
First I have general question. In a circuit with both logic and D edge flip flop does hold time have to satisfy $t_{hold} < t_{setup}($D-FF$) + t_{pd-min}$(Logic),
or is it enough that $t_{hold} \...
1
vote
0answers
17 views
Propositional extentionality in the lean theorem prover?
Propositional extentionality in the lean theorem prover is stated as the following axiom:
axiom proptext {a b : Prop} : (a $\iff$ b) \to a = b
My confusion about this is as follows: Previously I’...
2
votes
1answer
28 views
How do you correctly write this sentence as a CTL formula?
Sentence: From every reachable state it is possible to reach a state where $p$ is true.
How do you write this sentence as a CTL formula? So far I only dealt with CTL syntax and trees but maybe it ...
1
vote
0answers
28 views
Type theory based automated theorem prover?
I know that there exist type theory based proof-checker, and I know that there are logic/sequent-calculus based automated theorem provers.
But I haven’t heard of a type-theory based automated theorem ...
4
votes
1answer
60 views
A universal operator necessarily generates $\neg x$ for input $x,…,x$
I originally posted this on math.stackexchange, but then deleted it and moved it here since I think it would fit this site more.
I saw a claim in a slideshow from a basic computer architecture course ...
4
votes
2answers
121 views
Is there a way to convert a program into a Boolean formula?
Let's say I have a program P, in form of a binary code for x86 architecture.
I want to find a Boolean formula F (in form of CNF, or something like that), such ...
1
vote
1answer
109 views
Given a rng that outputs 0 or 1 with an equal probability, make a rng that generates 1 with a probability p
So this was an interview question I had a few weeks back that I just haven't been able to think of how to solve...
Given a random number generator that returns 0 or 1 with a 50% chance of either, ...
1
vote
0answers
30 views
How to minimize large DNF formula into deeper but smaller formula?
I want to minimize DNF formula which has ~200k products combined into a sum.
The depth of that formula is 2 - first level is the OR, and second level is AND for all conjunctions.
I have tried using ...
0
votes
1answer
32 views
Logic gate which checks if the input is a negative number and changes its output based on that
I need to create a HDL which will use logic gates to demonstrate if something is a negative number in two's complement. The input is 8 bits, while the output is 1 bit, and if the input is a negative ...
0
votes
1answer
17 views
What if an $L$-complete problem has $NC^1$ circuits? More generally, what evidence is there against $NC^1=L$?
What if an $L$-complete problem has $NC^1$ circuits? More generally, what evidence is there against $NC^1=L$?
