Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

4
votes
2answers
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 ...
4
votes
2answers
204 views

TQBF as interactive game

My teacher describes true quantified boolean formula (TQBF) as an interactive game between two players $\exists$ and $\forall$, and asks us to show a winning strategy for the existential player $\...
6
votes
2answers
4k views

Understanding DPLL algorithm

I'm trying to understand DPLL algorithm for solving SAT problem. And here it is: ...
1
vote
1answer
205 views

Why S=1, R=1 Is forbidden in RS-Flip Flop [closed]

I have come across about RS Flip Flop & I have tried implementing that on a simulator & using actual logic gates. But I'm still not sure whether I have correctly understood the case unstable ...
4
votes
0answers
140 views

Decidability over finite graphs of small degree [closed]

Suppose $\sigma$ is a vocabulary of First Order logic consisting of one binary relation $E$ and let $\phi$ be a $\sigma$ sentence (FO formula with no free variables). Is it decidable whether there is ...
1
vote
3answers
176 views

Loop Invariants as Tautologies

Would it be correct to characterize loop invariants as a type of tautology? I ask since the invariant must basically always be true, before the loop starts, before each iteration and after the loop ...
1
vote
1answer
192 views

Expressing complexity class P using first-order logic with LFP

Can anyone show how to express complexity class P using first-order logic with LFP? (descriptive complexity)
2
votes
2answers
109 views

Proving non-confluency and adding an equation to make it confluent and terminating

I currently have a system that has {f(a) = b, f(f(x)) = x} (part of an exam question - look at page 5 - exercise 1). To start off with proving non-confluency, I am ...
1
vote
3answers
344 views

Can P=PSPACE and PSPACE problems be formulated as $\Pi_1$ formula?

To say simply, can PSPACE problems be written as $\Pi_1$ formula? Or how can these problems be written in terms of (first-order) arithmetic hierarchy? edit:also currently, by what arithmetic ...
5
votes
2answers
786 views

Formulas vs Circuits

In boolean circuit complexity, a circuit is just defined by a Directed Acyclic Graphs with designated input and output nodes, where the intermediate nodes compute a specific boolean function. A ...
10
votes
3answers
558 views

anonymous lambda functions (functional programming)

What are anonymous (lambda) functions? What is the formal definition of an anonymous function in a functional programming language? In my simple terms, when I am programming in scheme/lisp I would ...
4
votes
2answers
231 views

Creating a logical circuit

Task: Design a 2 bit comparator. Input: 2x 2 bit (I take it as 2 2-bit values, let them be unsigned for simplicity) Output: 1 if result input1>input2 is true, 0 otherwise Develop truth table and ...
27
votes
4answers
4k views

Clear, intuitive derivation of the fixed-point combinator (Y combinator)?

The fixed-point combinator FIX (aka the Y combinator) in the (untyped) lambda calculus ($\lambda$) is defined as: FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. ...
1
vote
1answer
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 ...
3
votes
1answer
700 views

Description of resolution algorithm as it applies to SAT

SAT [5] 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 ...
2
votes
1answer
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 ...
3
votes
1answer
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 ...
7
votes
3answers
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 ...
2
votes
1answer
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 ...
4
votes
2answers
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 ...
13
votes
2answers
10k views

“Applicative order” and “Normal order” in lambda-calculus

Applicative order: Always fully evaluate the arguments of a function before evaluating the function itself , like - $(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x. x^2(2+1))\...
4
votes
1answer
1k views

Propositional formula in DNF can be decided in polynomial time?

For a given propositional formula f in DNF, one can decide in polynomial time, if the formula is satisfiable: Just walk through all subformulas (l_1 and ... and l_k) and check, wheter it has NO ...
3
votes
1answer
115 views

LTL: Show $\neg(aUb) \Leftrightarrow \neg b U (\neg a \land \neg b) \lor G \neg b$

I got as far as \begin{align} w \vDash \neg (a U b) &\Leftrightarrow \neg (w \vDash a U b) \Leftrightarrow \neg (\exists_{i\geq0} : w^i \vDash b \land \forall_{0\leq k < i} : w^k \vDash a) \\...
5
votes
1answer
398 views

How is verifying whether an assignment satisfies a boolean formula possible in polynomial time?

How can I prove that I can verify whether a boolean assignment of variables $a$ satisfies some boolean formmula $\phi$ in polynomial time? I know that we can just plug the boolean assignment into the ...
8
votes
1answer
129 views

Question related to Hilbert's 10th problem

Given $n \in \mathbb{N}$ and $p,q \in \mathbb{N}[x_1,\ldots,x_n]$ one can define the following formula in the language of formal arithmetics $$\varphi(n,p,q) = \forall x_1 \cdots \forall x_n : \neg ...
3
votes
0answers
266 views

Has someone seen this structure before?

I am working 1 with a certain structure, and I wonder if someone has seen it before. I am no mathematician, so all I can say is that I will do my best to describe this structure. It is actually very ...
10
votes
1answer
410 views

A programming language that can only implement computable bijective functions?

Are there programming languages(or logic) that can implement(or express) a function $f:\mathbb{N}\to \mathbb{N}$ if and only if $f$ is a computable bijective functions?
3
votes
1answer
114 views

Are two terms where one is without a $\lambda\beta$ normal form unconvertible in $\lambda\beta$?

I know that if you try and make the theory $$\lambda\beta+\{s = t\ |\text{ s, t are terms without }\lambda\beta\text{ normal forms}\}$$ then that theory becomes inconsistent. Are two terms where one ...
3
votes
1answer
438 views

Equivalence of GFp and Gp in LTL

In linear time logic, is $\mathbf{GF}p$ equivalent to $ \mathbf{G}p$ ? $\mathbf{GF}p$ means that it is always the case that p is true eventually. Let $\mathbf{G} p$ be defined as: $\forall j \ge0,\ ...
4
votes
2answers
264 views

First-order logic arity defines decidability?

I've read first-order logic is in general undecidable, and that could be decidable only when working with unary operators. (I think that's propositional logic, correct me if I am wrong) The question ...
1
vote
1answer
161 views

Resolution and incomplete Knowledge Base

Assume I have an incomplete knowledge base, for example: ...
3
votes
0answers
92 views

Spot the formalism (some kind of process logic)

Consider the following specification technique. A specification consists of a finite set of triples $\langle C, A, C' \rangle$, where $A$ is the name of an action and $C, C'$ are conditions, that is, ...
1
vote
1answer
101 views

Given the phrase “Where NONE of the following are TRUE” and two statements how should a boolean logic be composed?

Let's have two statements (value > 10) (value < 25) And a list of items with the following values 10 20 30 This is what a truth table would give ...
4
votes
1answer
326 views

Universality of NOT and CNOT

I'm trying to figure out why NOT and CNOT gates are not sufficient to create all bijective functions in classical circuits. I have been struggling on this for hours, and just can't make sense of it. ...
7
votes
2answers
2k views

Lambda Calculus simplification

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem. $$(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)(\lambda sz.sz)$$...
2
votes
1answer
4k views

How to make a parse tree for the following propositional logic formula?

I have a formula $ \neg((q \implies \neg q) \vee p \vee (\neg q \implies (r \wedge p))) $. As it contains 3 subformulas between the $\vee$'s, how can i put it into a parse tree, as a parse tree ...
5
votes
1answer
259 views

How many possible assignments does a CNF sentence have?

I'm having some trouble understanding the following: When we look at satisfiability problems in conjunctive normal form, an underconstrained problem is one with relatively few clauses constraining ...
2
votes
1answer
335 views

definition of formula validity

I read in some sources that valid formulas are tautologies (valid under every evaluation). In the others, I read that these are formulas that have conclusions true when premises are true. Are these ...
7
votes
1answer
245 views

Redundancy elimination in the superposition calculus

When proving theorems with the superposition calculus, we deal with three kinds of rules: Generating rules: from pair of clauses A and B, generate new clause C while keeping the original pair, e.g. ...
2
votes
1answer
1k views

Negation of nested quantifiers

The problem is: $$\exists x \forall y (x \ge y)$$ With a domain of all real positive integers. The negation is: $$\forall x \exists y (x < y)$$ so, if $y = x + 1$, the negation is true. That ...
0
votes
2answers
377 views

Predicate Logic Paradox [duplicate]

Possible Duplicate: Negation of nested quantifiers The problem is: ∃x∀y(x ≥ y) With a domain of all real positive integers. The negation is: ∀x∃y(x < y) so, if y = x + 1 the negation is ...
6
votes
2answers
206 views

The meaning of modulo in “formula modulo a background theory”

I have been reading some papers where I keep reading stuff like “first-order formula modulo a background theory”. Does anyone know what modulo means in this case ? Is it something like “with respect ...
10
votes
1answer
455 views

Distinct variables for different clauses

In resolution theorem proving, it is normally assumed variables in different clauses are distinct. This is not something that happens automatically; it requires significant extra code and computation ...
5
votes
1answer
114 views

Is the validity of some instance of an equational problem decidable?

Is the following FOL-problem (equality is a logical symbol) effectively decidable? Given. A finite equation system $E$ and an equation $s = t$. Question. Is there a substitution $\sigma$, such ...
5
votes
1answer
303 views

Free variables of (λx.xy)x and bound variables of λxy.x

I was solving exercises on Lambda calculus. However, my solutions are different from the answers and I cannot see what is wrong. Find free variables of $(\lambda x.xy)x$. My workings: $FV((\lambda x....
8
votes
1answer
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 ...
8
votes
2answers
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 ...
9
votes
2answers
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 ...
15
votes
4answers
623 views

Is there a repository for the hierarchy of proofs?

I am self-learning proof assistants and decided to start on some basic proofs and work my way up. Since proofs are based on other proofs and so form a hierarchy, is there a repository of the hierarchy ...
5
votes
1answer
1k views

Validity of predicate logic formulas

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 ...