# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

664 questions
2k views

### Why do ¬, ∀ and ∃ have the same precedence?

I thought the order of precedence of operators and quantifiers was arbitrary, but I don't really understand why those three have the same "strength" in relation to other operators (e.g., ¬ will have ...
19 views

### How do I get the NAND gate configuration for full adder from the logic table?

I'm self-studying, but I've gotten stuck already. If I'm given the logic table for a full-adder or any two-output table, how do I figure out the NAND-gate configuration, preferably methodically? ...
84 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)?
16 views

### Can we ignore the postcondition in the Hoare conditional rule when there is a return statement?

I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode: ...
46 views

91 views

### Interesting logic problems

I've just began a course on logic and learned the following : De Morgan's laws Normal forms How to represent a logical formula (using or, and, not operators) using binary trees How to ...
74 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 ...
148 views

### Decidability of equivalence to existential formulas

I'm looking for an algorithm to decide 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 ...
57 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 ...
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 ...
42 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 ...
52 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 ...
46 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 ...
42 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 ...
21 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 ...
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 ...
97 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 ...
32 views

24 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 ...
31 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=...
36 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 ...
39 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 ...
184 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 ...
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 ...
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$?
291 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 ...
40 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 ...
38 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. ...
69 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 ...
125 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 ...
30 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 = ...
403 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 ...
29 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 ...
42 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 ...