# Questions tagged [first-order-logic]

First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.

221 questions
Filter by
Sorted by
Tagged with
1 vote
20 views

### How do I prove relations of two CTL formulas?

If I have two CTL equations, how do I prove they're equivalent or that one implies the other? What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
167 views

### how to do incremental construction of the minimal model in logic programming?

I was reading a book titled "Essentials of Logic Programming.", most parts of the book are easy to understand. but now having a problem with Theme 45: incremental constructions of the ...
51 views

### Is any 2-CNF has 2-DNF representation?

I was asked a question whether I could come up with a 2-CNF over several variables that has no 2-DNF representation. However I thought that any CNF can be converted to DNF through some manipulations e....
16 views

### Is first order linear temporal logic a special case of first order modal logic?

Propositional linear temporal logic is a special case of propositional modal logic. Is first order linear temporal logic likewise a special case of first order modal logic?
144 views

### Can you help me in finding an algorithm that finds the first unique number in an array with lowest position?

I have the following problem to solve: Given a non-empty array A consisting of N integers, the task is to find the first unique number in the array. A unique number is defined as a number that occurs ...
68 views

### 'Someone' in first order logic

I have in the lectures a sentence in English, which I have to translate to First Order Logic. Someone who loves all animals loves all humans. Textbook solution: ∀x.(is_human(x) ⇒ is_animal (x)) ⇒ ∀...
41 views

### Minimum DNF length of a conjuction of equivalences

Show that the formula $\bigcap_{i=1}^n (X_i \leftrightarrow Y_i)$ cannot have an equivalent disjunctive normal form with less than $2^n$ clauses. I am puzzled on what approach to take -- whether to ...
1 vote
43 views

### Understanding unprovable halting, model theory, and (in)completeness

I know computability, but not model theory and logic, so this question may be naive or confused in that respect. A blog post of Scott Aaronson mentions a Turing Machine $M^*$ such that the statement P:...
40 views

### How substituituion composition is associative?

I'm not convinced that substitutions are associative, I read the https://en.wikipedia.org/wiki/Substitution_(logic)#First-order_logic and the https://www.youtube.com/watch?v=_cVNeccMF-E My problem is ...
1 vote
50 views

37 views

### First-order model checking is not fixed parameter tractable on general graphs

I read that the problem of first-order model checking is believed to be not fixed parameter tractable on general graphs. Why is this the case? Would be happy about some reference Thanks in advance!
1 vote
24 views

### Prove that any first-order logics with equality and a relation/functional symbol of arity more than 1 is undecidable

Definition: A formal logic system is decidable – if there is an algorithm that can determine if any given sentence is a theorem (or not). Based on this definition, I am not sure how to move to prove ...
85 views

### Is there a quantifier more powerful than the other to determine FOL connector?

So basically we have 2 types of quantifier in first order logic, they are universal quantifier and existential quantifier. Usually we use implies connector(->) when we have universal quantifier in ...
22 views

### How can I prove KB╞ α?

Is correct to use ~α as rule to prove KB╞ α? Is possible to unify sentence ~V(x,y) v S(x) with V(N,W)? ...
1 vote
34 views

### First-order iteration operator example

I am reading on https://en.wikipedia.org/wiki/FO_(complexity)#Iterating that FO[$t(n)$] consists in first-order logic with an iteration operator that iterates $t(n)$ number of times some quantifier ...
65 views

### Conjuctive Normal Form

Let f(P,Q,R) be the truth-function defined as follows. f(P,Q,R)=1 if and only if Q and R have different truth-values; or P and R have the same truth-values. Choose all formulas that are in conjunctive ...
76 views

### Resolution algorithm does not seem to generate the empty clause

Let's assume I have the following 3 clauses: $\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$ and I want to see if our KB entails $\neg U$ so I tried to apply ...
40 views

### Why is “For all the simple things you have done to me, there exists one thing that makes me happy” FALSE? Use nested quantifiers to prove your point

I've done my due dilligence and tried to answer this question using every resource I could get. KhanAcademy, NesoAcademy, and Rosen's Discrete Mathematics book. I still can't wrap my head around it. ...
74 views

### Uses of of the one-variable fragment of first-order logic aka S5

I'm looking at decidable fragments of first-order logic. It seems that FO(1), i.e. the one-variable fragment of first-order logic is equivalent to the modal logic S5. However, I cannot find a ...
34 views

### Specific quantifier elimination for real algebraic numbers

It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
1 vote
50 views

### Restriction in description logic

$Human ⊓ ¬Female ⊓ (∃married.Doctor) ⊓ (∀hasChild.(Doctor ⊔ Professor))$ Here, $∃married.Doctor$ means if there exists an individual who is married to Bob belongs to $Doctor$ concept. But my ...
63 views

1 vote
74 views

54 views

### Do FOL theorem provers accept axiom schemata?

Axiom schemata (such as ZFC) are, in a sense, infinite sets of axioms. Do the ATPs designed to work with FOL (such as Vampire) accept axiom schemata? I looked in the Vampire "manual" briefly,...
1 vote
45 views

### Help me understand whether these critical pairs are joinable

I have the following TRS $R$: $$l_1 = f(g(x)) \to f(x) = r_1 \\ l_2 = g(f(y)) \to g(y) = r_2$$ I want to know if $R$ is confluent, and whether $g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$. I have ...
1 vote
52 views

### What is the space-complexity of a boolean first-order query?

I have the intuitition that, if we implement a (space-efficient) boolean first-order query solver, the amount of consumed memory should depend on the data size (i.e., it should not be constant). ...
In Turing's 1936 paper On Computable Numbers Page 30-31, and its Correction Page 1-2 : For a Turing Machine $M$, $Inst(q_i S_j S_k L q_l )$ means that if $M$ scans symbol $S_j$ under \$m-...