Stack Exchange Network

Stack Exchange network consists of 175 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

5
votes
2answers
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 ...
1
vote
0answers
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? ...
1
vote
3answers
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)?
1
vote
0answers
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: ...
2
votes
1answer
46 views

Negation of the semantics of the Until operator in LTL

I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to: $\phi R \psi \equiv \neg(\neg\phi U \neg \psi)...
1
vote
1answer
34 views

Turing Machine where branches are resolved via arbitrary operator

Alternating Turing Machines output Boolean values and combine the values returned by branches via the any/all operators. Is ...
1
vote
2answers
54 views

If a NAND gate is universal, why you don't have NAND OISCs

If a NAND gate can be used to construct all other of the basic logic gates, then I'm wondering why you don't/can't have a purely NAND-based One Instruction Set Computer (OISC). All the OISC single ...
0
votes
0answers
33 views

Can we see all of mathematics as an attempt to simplify computations?

This is a rather strong claim, and therefore likely to be incorrect, but hear me out. Firstly, when I talk of “computations”, I mean this in a broader sense than normally used, because I am including ...
1
vote
1answer
23 views

(Generally) How to specify asynchronous action with side effects using logic equations

Say you have this function call sequence: function all() { fn1() fn2() fn3() } And say that fn2 was asynchronous and ...
2
votes
1answer
36 views

Examples of logic gates using non-standard models

These are the only ones I have been able to find online: Pulley Logic Gates Marble adding machine MARBLE COMPUTER LOGICAL AND GATE I would like to find some more discrete models like these (as ...
0
votes
1answer
19 views

LTL to Büchi automaton, deterministic?

I know it is possible to convert LTL formulas to Büchi automatons. But is it possible to convert a LTL formula to a deterministic Büchi automaton? Are there formulas that can't be converted to a ...
2
votes
1answer
17 views

How to understand the notion of boolean query via Immerman's definition

A query is any mapping $I:STRUC[\sigma] \to STRUC[\tau]$ that is polynomially bounded. A boolean query is a map $I_b: STRUC[\sigma] \to \{0,1\}$. A boolean query can also be thought as the susbset: $...
3
votes
2answers
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 ...
1
vote
2answers
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 ...
2
votes
1answer
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 ...
5
votes
2answers
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 ...
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
1answer
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 ...
0
votes
2answers
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 ...
1
vote
1answer
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 ...
1
vote
1answer
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 ...
0
votes
0answers
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 ...
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
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 ...
0
votes
2answers
32 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
1answer
97 views

Does every 3CNF propositional formula has an equivalent 2CNF propositional formula?

Does every 3CNF propositional formula has an equivalent 2CNF propositional formula? Definitions: 3CNF propositional formula is conjunctive normal form propositional formula, which is just ...
3
votes
3answers
92 views

Linear Temporal Logic with non-Boolean propositions (e.g. Integers)?

LTL works with Boolean propositions. People probably studied extensions to non-Boolean propositions... Do you know a good starting reference? (I am aware of STL, but it also seems to talk about ...
1
vote
0answers
17 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
186 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 ...
6
votes
2answers
145 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
28 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
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 ...
0
votes
1answer
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=...
0
votes
1answer
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 ...
2
votes
1answer
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 ...
9
votes
2answers
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 ...
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
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 ...
0
votes
1answer
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 ...
0
votes
1answer
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. ...
3
votes
1answer
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 ...
4
votes
2answers
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 ...
1
vote
1answer
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 = ...
13
votes
1answer
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 ...
1
vote
0answers
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 ...
1
vote
1answer
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 ...
1
vote
2answers
835 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
114 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
20 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 $...