Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

695 questions
67 views

LTL to automaton translation that can only read disjunctions of labels per transition

Is there any automaton (or automaton translation) as expressive as LTL that can only read disjunctions of atomic propositions per each transition? Standard LTL-to-automaton algorithms allow the ...
56 views

box bottom is valid

This question was posted to me: What property of our relation $R$ between worlds must be true if we know that the following formula is valid? $\square \bot$ I am completely stumped and have no idea ...
87 views

Complexity of Solving a System of Polynomial Equations

It can be easily seen that solving systems of polynomial (i.e. not necessarily linear) equations is NP-Hard via reduction from SAT. Furthermore, because the existential theory of the reals is ...
5k views

What exactly is a logic?

An apology might be in due for asking another question about prerequisites, but I was confused about the starting points. I have come across various terms such as "Modal Logic", "Temporal logic", "...
271 views

Is Agda sound as a proof system?

I was browsing Agda's stdlib source code, since I was trying to get into it seriously and therefore wanted to know more. I was amazed at that Agda is way more developed than I thought and it's ...
121 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). ...
58 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" ...
61 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): ...
76 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 ...
88 views

Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
427 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 ...
33 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 ...
82 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 ...
1k 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 ...
71 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 ...
38 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? ...
291 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 ...
723 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-...
201 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 ...
1k 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)
72 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

69 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 ...
204 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 ...
82 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 ...
51 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 ...
114 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/...
285 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$ ...
91 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?
321 views

Logic Circuits - Binary divisible by 16 [closed]

I have a question ...
389 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}(\...
64 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.
383 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'...
89 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, ...
96 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 ...