Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

695 questions
81 views

Temporal logic for interface invariants

I am looking for some sort of temporal logic for expressing invariants in interfaces. Since interfaces do not specify data representation, the invariants must rely solely on the publicly available ...
204 views

849 views

Difference between intended interpretation and extended interpretation in first-order logic

I am currently reading "Artificial Intelligence - A modern approach" and I really do not get the difference between intended interpretation and extended interpretation in first-order logic. Are ...
700 views

Description of resolution algorithm as it applies to SAT

SAT  can be solved with resolution definitively, i.e. if the formula has a true assignment, resolution can find it, and if it cant be satisfied, resolution can show that no assignment exists (at ...
303 views

Building functionally complete boolean circuits out of trinary logic

There are some not-very-commonly considered forms of trinary logic using 3 truth values. Even entire (unusual/rare) ternary computers have been built from it. Is there some knowledge or reference ...
553 views

MGU and Variable Standardization - CNF

I have been reading on converting first order logic sentences to conjunctive normal form, and then performing resolution. One of the steps of converting to CNF, is to Standardize variables: rename ...
4k views

Is resolution complete or only refutation-complete?

Going through some knowledge representation tutorials on resolution at the moment, and I came across slide 05.KR, no77. There it is mentioned that "the procedure is also complete". I think this ...
179 views

Convert CTL* formula to CTL

I have a CTL* formula: $\mathsf{EF}[p\land \mathsf{AX}[q\ \mathsf{U}\ r]]$ but in my application, I am limited to CTL. To my understanding, this formula is no valid CTL and I wonder whether I can ...
11k views

The difference between a sequence and a set

I am new to discrete mathematics and the theory of computation I am trying to learn and understand the terminology. I am having a difficult time understanding the difference between a set and a ...
10k views

261 views

How much can we reduce the number of clauses by converting from $k$-SAT to $(k+m)$-SAT?

If we suppose that we start with an instance of $k$-SAT, and try converting the problem to an instance of $(k+m)$-SAT, where there are $(k+m)$ literals per clause, can we guarantee a reduction in the ...
384 views

A tentative satisfiability algorithm

General satisfiability (with a few exceptions such as Horn Clauses) is not believed to have an algorithmic solution. However, the following algorithm appears to be a solution for general ...
414 views

Introduction into first order logic verification

I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
The following predicate logic formula is invalid (i.e. not a tautology): $\Bigl[\forall x \,\exists y {\,.\,} P(x,y)\Bigr] \implies \Bigl[\exists y \, \forall x {\,.\,} P(x,y)\Bigr]$ Which of the ...