# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

640 questions
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). ...
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" ...
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): ...
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 ...
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): ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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? ...
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 ...
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 ...
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-...
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 ...
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)
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\}$ ...
57 views

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 ...
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. ...
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 ...
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 ...
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 ...
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/...
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$ ...
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?