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

4
votes
1answer
91 views

SAT Solver Front-End: Strategy to order Quantifiers

I am working on a small project. The goal is to implement a compiler from a quite simple, custom syntax of logical formulae (including variables over finite domains) to conjunctive normal form (CNF). ...
1
vote
0answers
45 views

What is the definition of the property of Canonicity for a logic?

I'm trying to understand "A Systematic Approach to Canonicity in the Classical Sequent Calculus" by Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. The article discusses a property called "canonicity" ...
0
votes
1answer
56 views

Inference rules for deriving invariants in Hoare logic

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
1
vote
1answer
72 views

Classical set theory and the existence of at least one set

As a student of mathematics I used to accept the argument that the existence of the empty set followed from the axiom schema of comprehension, so long as we could prove the existence of at least one ...
4
votes
1answer
84 views

Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
3
votes
2answers
366 views

Propositional Logic Time complexity

If i have a propositional logic formula, every time i add a variable the number of interpretation grow up by 2. So if i have a propositional formula with 3 variables i have 8 interpretations. So, is ...
1
vote
1answer
28 views

Semidecidability and NP-Hard

Im studying the semidecidability of First Order logic. According to wiki A logical system is semidecidable if there is an effective method for generating theorems (and only theorems) such that ...
0
votes
1answer
41 views

SAT solver optimizations of DPLL for unsatisfiable formulas [duplicate]

I am implementing a SAT solver based on DPLL algorithm, and it works fine on small formulas and larger satisfiable problems. My case split is based on a tree like structure, where every branch is ...
5
votes
2answers
864 views

Equisatisfiability in the reduction from 4-SAT to 3-SAT

So If I understood correctly, the conversion from 4-SAT statement to 3-SAT statement follows the following approach: (a or b or c or d) -> (a or b or z) and (-z or c or d) Where the z is a new ...
0
votes
0answers
67 views

Is it possible for a [futuristic] computer to contain the information of the whole universe?

(This is a question of information theory, data compression and entropy, so I believe it fits CS forum) Does the fact that the computer itself is a part of the universe make it logically impossible ...
18
votes
4answers
5k views

Can proof by contradiction work without the law of excluded middle?

I was recently thinking about the validity of proof by contradiction. I’ve read for the past few days things on intuitionistic logic and Godel’s theorems to see if they would provide me answers to my ...
12
votes
5answers
2k views

Why does soundness imply consistency?

I was reading the question Consistency and completeness imply soundness? and the first statement in it says: I understand that soundness implies consistency. Which I was quite puzzled about ...
0
votes
0answers
31 views

Description logic representation

If Manufacturer manufactures electronic equipment, then manufacturer generates e-waste. I have generated the triple. However how to represent the if-then statement in DL? ...
5
votes
1answer
222 views

Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence

I have to ask for forgiveness in advance if the whole question doesn't make a lot of sense, but unfortunately, I have no better intuition as of right now and this seems like the best starting point I ...
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 ...
1
vote
2answers
386 views

how to solve Hoare logic problems

I'm having trouble proving Hoare logic questions as I'm not sure of the process that is taken to prove them. I understand that they're rules such as assignment axiom, pre-condition strengthening, post-...
2
votes
2answers
136 views

A 4-bit combinatorial circuit that outputs 1 when integer greater than 7 and is odd number

I need to draw a combinatorial circuit that when an integer is greater than 7 and is an odd number, the output will be 1. There are 4 inputs representing 4 bits and 1 output wire. The output wire is ...
0
votes
1answer
796 views

Proof of Demorgan's law [duplicate]

how can i prove Demorgan's law (X+Y)'=X'. Y'?I already tried studying book but doesn't understand the first step so plz answer in detail.(beginner here)
0
votes
1answer
67 views

Does exist NP language that is Cook Levin deterministic reducible to xor satisfiability in polynomial time?

We say that the language $L$ is Cook Levin deterministic reducible to xor satisfiability in polynomial time if and only if for each word $w\in\Sigma^*:w\in L\iff f(w)\in XORSAT$ where $\Sigma=\{0,1\}$ ...
2
votes
1answer
57 views

Why is $AF \phi \lor \varphi$ not equivalent to $AF \phi \lor AF \varphi$?

Can someone explain to me (perhaps with an example) why $AF (\phi \lor \varphi)$ is not equivalent to $AF \phi \lor AF \varphi$. This seems counter-intuitive, because in any path where $\phi$ (or $\...
0
votes
1answer
106 views

Is this possible to solve satisfiability by using Quine McCluskey algorithm to simplify the whole given boolean formula by simplifying subformulas?

In this question Farewell Stack Exchange suggested to use karnaugh maps to solve the satisfiability problem by simplifying the entire/whole boolean formula by simplifying subformulas until you have ...
0
votes
2answers
529 views

Which of the following expressions is TRUE if and only if NOT all three variables a, b, and c have the same value?

I am trying to solve this problem and I am stuck. I think it is B, but I think I'm wrong. Thanks. Which of the following expressions is TRUE if and only if NOT all three variables a, b, and c have ...
0
votes
1answer
959 views

Finding weakest precondition

I have the following program x := y + 1; if (y > 0) then x := x + y else x := y + 100; x := x + y; I want to compute the weakest precondition for getting <...
1
vote
1answer
91 views

LTL Until Tautology

Today I had to prove some tautologies as an exercise, one of them was: (Ga)->(Fb) equivalent aU(b v ¬a) It is clear that I have to prove the implication in both ways. After putting into negation ...
2
votes
1answer
42 views

LTL Formula Until with same atoms (aUa)

I am trying to solve some past papers in preparations for my next exam and I've stumbled across the following exercise: While I managed to solve most parts of the exercise, I am still unsure about ...
5
votes
1answer
139 views

Lambda calculus as the language of universal logic - connectives vs functions in lambda calculus?

I am reading http://okmij.org/ftp/gengo/applicative-symantics/AACG1.pdf and there is defined language TL (see last row in the table on page 4). It seems to me from this definition of TL, that lambda ...
0
votes
0answers
36 views

Finding the value of y for given equation?

Given the equation : x & y = x, where x, y are positive integers. Note: Here '&' stands for Bitwise operator AND between two numbers. I am provided with the value of x. Can I find possible ...
3
votes
3answers
174 views

Does exist any horn formula that is equisatisfiable to the clause that is disjunction of two literals? Does also exist equivalent?

I just and simply want to know if whether or not exist any horn formula that is equisatisfiable to $(p\lor q)$. I would also be interested to know if there also exists equivalent.
2
votes
1answer
64 views

Why doesn't this put $BPP$ in $NP$?

From Sipser Gacs we know $x\in L(M)$ for a machine $M\in BPP$ $\iff$ $$\exists t_1,\dots,t_{|r|}\forall r\in\{0,1\}^{|r|}\vee_{i\in\{1,\dots,|r|\}}M(x,r\oplus t_i)=1.$$ From Adleman we know $x\in L(M)...
3
votes
1answer
59 views

Validity of this formula in WS1S logic

The following formulas are said to be defined in WS1S logic. $Closed(Z, R) := ∀x ∀y(x ∈ Z ∧ R(x, y) → y ∈ Z)$ $(z_1, z_2) ∈ R^∗ := ∀Z.(z_1 ∈ Z ∧ Closed(Z, R) → z_2 ∈ Z)$ However since WS1S formula ...
1
vote
1answer
140 views

Explanation of the Gelfond Lifschitz reduct

Can someone explain with a hands on example how the Gelfond Lifschitz reduct works in order to check stable model semantics? edit a simple example here - at least as far as I understand the thing. ...
1
vote
0answers
23 views

how to use the solution of mean payoff game to arrive at winning regions of parity game?

The 7th chapter (7.3 section) of "Automata Logics and Infinite Games" by Erich Gradel, Wolfgang Thomas, Thomas Wilke gives a way to convert max parity game to mean payoff game. I do not understand ...
3
votes
1answer
73 views

Programmatically checking equivalence of statements

So as part of a theorem-prover/checker, I'm using Prolog to try to determine the equivalence of statements that have been parsed into tree form, e.g. $x=2$ is represented as ...
2
votes
0answers
50 views

Automatic learning/discovery of logics

Are there efforts to automatically discover new logics? Logics are simple structures - they have formal language, deduction rules, semantics and certain properties that are proved or discarded for ...
3
votes
0answers
73 views

Semantic parsing with Grammatical Framework - is this possible?

So far I have learned about categorial grammars, type logical grammars and formal semantics of natural language, the relevant tools are Cornell Semantic Parsing Framework https://github.com/clic-lab/...
-1
votes
1answer
279 views

Must algorithm for comparing numbers investigate all bits?

Suppose algorithm $A$ on a digital computer takes as input integers $x$ and $y$ in binary. The algorithm outputs one if $x=y$, and zero if $x \neq y$. Is there a proof that for any input $x$ and $y$ ...
1
vote
1answer
77 views

Proving that a Turing machine decides a language in NP

Suppose a deterministic Turing machine T decides language L and L is in NP. Then must it be provable in ZF that T decides L?
0
votes
1answer
261 views

Logic Circuits - Binary divisible by 16 [closed]

I have a question ...
2
votes
2answers
230 views

Max() in Domain Relational Calculus

I was looking through my notes on domain relational calculus, and noticed an interesting result in a question about finding the most expensive pizza(s), given a pizza table with schema $\text{pizza}(\...
0
votes
1answer
54 views

Given two formulae E[G F p] (which is CTL*) and EG EF p ( which is a CTL) with a Model prove that they are not equivalent

I am trying to prove they are not equivalent , a model which satisfies the fist one but not the second since I think EG EF p is stronger than E[GF p],any leads would be helpful. Thanks.
0
votes
2answers
287 views

Two's complement 8-bit subtractor? [closed]

Please help me! I've been asked to make a circuit using only Logic Gates to implement an 8-bit 2's complement subtractor. I was thinking of somehow modifying an 8-bit adder, but I figured it isn't 2'...
3
votes
0answers
63 views

Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ...
1
vote
1answer
78 views

Complexity of 1-in-3 SAT variant with restrictions on “unique” variables per clause

I'm interested in the complexity of a particular variant of 1-in-3 SAT. Assume, as is usual, that clauses are allowed to be of length 1, 2, or 3. Then add the restriction that for any clause of length ...
0
votes
2answers
98 views

How to convert 2 or gates (x1 V x2 V x3) to NAND

How can I convert a clause of size 3 that is made of 2 OR gates example: (x1 OR x2 OR x3 ) to one or more clauses of size 4 made only of NAND ...
1
vote
3answers
107 views

How does maths consistency impacts on computer science?

Lot of mathematicians have made several efforts to answer the question : are mathematics consistent ? Although we haven't yet had a proof of consistency, and surely we will never (Gödel second theorem)...
2
votes
1answer
195 views

Draw a function by only using two input NOR gates [closed]

T = (BD + A'BC'+A'CD) How can i draw this by only using NOR-Gates? This is what i have done so far: https://imgur.com/a/JG2eU Have I understood this right?
1
vote
0answers
49 views

Hoare correctness proof for a recursive definition of multiplication

Given the program: {y=y0 ^ y>=0} z=0; while (y>0){ z=z+x; (1) y=y-1; } {z=x*y0} I am having trouble finding the ...
5
votes
2answers
156 views

Undecidable predicate logic is decidable by people?

Logic in computer science (By Michael Huth,Mark Ryan, second edition, page 132) says Every φ can, in principle, be discovered to be valid or not, if you are prepared to work arbitrarily hard at ...
4
votes
0answers
36 views

Modern presentation of Ackermann's “Solvable Cases?”

Ackermann's book "Solvable Cases of the Decision Problem" discusses decidable instances of first order logic, particularly monadic logic, and so called "equality formulas". However, the book is from ...
1
vote
1answer
58 views

What is the transitive and reflective closure of the derivation relationship?

This question is asked during a class of Computer Science. What is the transitive and reflective closure of the derivation relationship? I know that if $R$ is a relationship on $A^2$, a ...