# Questions tagged [first-order-logic]

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

204 questions
Filter by
Sorted by
Tagged with
19 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 ...
10 views

### What could be a good reference for types and tables in First Order Logic?

My research caters mostly to Statistical Relational Learning community, so Probability + Logic. I would like to provide a reference for the concept of types and tables in First-Order Logic, as ...
34 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 ...
10 views

### Convert referent of an sentence into an if statement

I was reading Deductive logic in Natural Language.It said that meaning of sentence depends on meaning of words. My question is that can this technique be used along with set theory to convert the ...
30 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. ...
39 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 ...
26 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 ...
38 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 ...
48 views

56 views

47 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,...
38 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 ...
20 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). ...
40 views

67 views

### Sample applications based on First Order Logic

I often hear about benefits of FOL, but I wonder what are some of its real world applications? Could someone please provide samples/case studies of applications of FOL that address real world ...
29 views

### In first order logic, how do we normally represent a statement?

I wanted for an example such as: Everyone has a mother. I've seen that it is represented in FOL as: $\forall x \exists y:$ Mother(x, y) I'm seeing that as:For every x, there exists a y, such that y ...
147 views

### Proving a first order logic theorem in equational logic with a term rewriting system

I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean ...
statement 1: $Γ$ is satisfiable implies $Γ$ is consistent. statement 2: If $Γ$ derives $α$ then $Γ$ entails $α$. I can easily prove statement 1 from 2 , but not 2 from 1 (without using strong ...
Assuming you have a formula in first order logic like $$(\forall_x p(x) \land \forall_x q(x)) \rightarrow \forall_x(p(x) \land q(x))$$ (which seems valid?) Converting the formula to ...