Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

0
votes
1answer
20 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
22 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 ...
2
votes
1answer
33 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 ...
0
votes
0answers
12 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 ...
9
votes
2answers
179 views

What is the current status of parallel or concurrent programs in the Curry-Howard isomorphism?

In Girard's Proofs and Types we can read : From an algorithmic viewpoint, the sequent calculus has no Curry-Howard isomorphism, because of the multitude of ways of writing the same proof. This ...
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$?
7
votes
2answers
243 views

What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
0
votes
1answer
36 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 ...
0
votes
1answer
34 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. ...
3
votes
1answer
61 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 ...
4
votes
2answers
120 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
25 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 = ...
13
votes
1answer
378 views

The difference between dynamic logic and temporal logic

To find the difference, I'd just encountered with assertions below about temporal logic in Wikipedia: another variant of modal logic sharing many common features with dynamic logic, differs from ...
1
vote
0answers
23 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 ...
6
votes
2answers
138 views

propositional Modal logic filtration definition

Hello I have a slightly unusual question which relates to a definition of filtration structure. The following is my current state of the definition: $ \mathcal{M} = (W, R, L) $, W is a set of worlds, ...
1
vote
1answer
37 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
14 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\ ...
1
vote
2answers
796 views

Do quantum logic gates work differently than traditional logic gates?

In a traditional computer calculations are done with logic gates that check inputs with AND gates etc. But in a quantum computer, are calculations performed differently since the qubit can be in ...
0
votes
1answer
91 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
17 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
64 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$...
1
vote
2answers
66 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
31 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
9 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
22 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 ...
3
votes
0answers
49 views

Finiteness of the set of equivalence classes of formulas generated by boolean combination

Define a relation $\equiv$ on the set of modal formulas by $\phi \equiv \psi \Leftrightarrow (\forall M\forall w, M,w \models \phi\Leftrightarrow M,w \models \psi)$ (so it is an equivalence relation) ...
1
vote
3answers
88 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 ...
2
votes
1answer
114 views

First Order Logic : Predicates

I have a small problem with the first order logic, in particular, predicate logic Let us take this sentence as an example: ...
0
votes
4answers
120 views

Simplifying a boolean expression

I need to prove: XY + ~XZ + YZ = XY + ~XZ I cannot think how to do this. I have tried factorising, but I just don't know of any rule that removes one of the ...
13
votes
1answer
278 views

“Famous logicians have made embarrassing errors here,” a line from SICP. What is this referring to?

Here is the context (Structure and Interpretation of Computer Programs, section 1.1.8, under heading "Local names"): A formal parameter of a procedure has a very special role in the procedure ...
1
vote
1answer
35 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
26 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
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} \...
0
votes
0answers
8 views

Determining the max frequency of a cycle with flip flops

The following cycle is given and i need to determine what is the max frequency possible for it. The cycle has 3 positive D-edge Flip Flops and some logic gates. i calculated the time it takes for ...
0
votes
1answer
32 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
114 views

Can the foundation of computer science be implemented to include new rules of inference so that computer can do causal reasoning?

The idea I'm thinking of is about a top-down approach for AI. I would like to know if there can be a model for computers so that they can perform causal reasoning. It seems that causal relation can be ...
0
votes
0answers
21 views

How express this short sentence in CTL?

It's possible that in some following state you have that $x,y$ are both true simultaneously. I have taken a look on Wikipedia: https://en.wikipedia.org/wiki/Computation_tree_logic and if I ...
1
vote
0answers
16 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
27 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
56 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 ...
1
vote
1answer
4k views

Drawing an implication graph for 2-SAT clauses

I am trying to convert the following 2-sat clauses to implications and then draw the implication graph. The clauses are: ...
1
vote
1answer
62 views

Relational calculus to SQL

I am somewhat aware of the correspondence between (tuple and domain) relational calculus, relational algebra, and SQL. To the best of my understanding, one should be able to automatically convert a ...
1
vote
1answer
104 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, ...
0
votes
1answer
29 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 ...
1
vote
0answers
26 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 ...
5
votes
5answers
1k views

XOR two numbers

Is there an intuitive meaning of XOR of two numbers not involving binary and just decimal? Or is is always converted into binary and then XORed?
3
votes
1answer
86 views

Detect non existence of a cycle in a graph using Datalog : SMTLIB Format for Z3

I want to detect the non existence of a cycle in a graph using Datalog (which is a declarative logic programming language). The proposed solution was: ...