# Questions tagged [first-order-logic]

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

181 questions
Filter by
Sorted by
Tagged with
163 views

### Decidability of equivalence to existential formulas

I'm looking for an algorithm to decide if a given first order formula over a fixed vocabulary admits a logically equivalent existential one (i.e. a formula in prenex form where all quantifiers are ...
44 views

### Refutation in first order logic

Consider the following statement In FOL, we can reduce entailment checking to satisfiability checking: $S \models S' \iff S \land \neg S'$ is satisfiable (This proof strategy is called ...
193 views

### Does every 3CNF propositional formula has an equivalent 2CNF propositional formula?

Does every 3CNF propositional formula has an equivalent 2CNF propositional formula? Definitions: 3CNF propositional formula is conjunctive normal form propositional formula, which is just ...
31 views

### Superposition calculus: greater vs greater-or-equal

Bachmair and Ganzinger 1991, 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', specifies the criterion for using an equation as, by some appropriate ordering, ...
40 views

### Superposition calculus: Elimination of redundant atoms

Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', section 5.2, 'Simplification and Deletion Techniques', page 17, 'Elimination of redundant ...
29 views

### Bachmair and Ganzinger, ordering of equations

Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', page 4, defines an order on equations. (This is an arcane piece of machinery but a critical ...
300 views

### Real world applications of first order logic

I study an AI course and we done some lectures about first order logic and the first thing that I was thinking is, what are the real world applications of first order logic and generally logical ...
100 views

### Why Modus ponens works with Horn clauses and Generalized Modus ponens requires definite clauses?

I am reading the Artificial Intelligence: A Modern Approach book and in the chapters about logic i noticed that in propositional logic the Modus ponens inference rule (used by the forward and backward ...
154 views

### Logical and non logical symbols and predicates

I am going through the text from "R.Brachmann and H.Levesque: Knowledge representation and reasoning". Here it has been described(in page 15) that there are two types of symbols : the logical symbols ...
166 views

### Does this Haskell code represent a decision procedure for a theorem?

The following is a natural language description of a first order theory from Worboys. Only Axiom 11 and the Theorem 4 are written in mathematical notation. Theory 1 Aland, Bland, Cland, and Dland are ...
16 views

### Why the given statement can't be expressed using predicates and quantifiers in the way described in details?

Suppose there is a statement - Some students in this class has visited Mexico. Solution given is: considering the universe of discourse for the variable $x$ consists of all the people. Our ...
72 views

### Must $x$ and $y$ be different in a statement of the form $\forall x \forall y \cdots$?

Given the following predicate formula $F$: $$\forall x \forall y [(\text{italian}(x) \Rightarrow (\text{winWC}(y) \Rightarrow \text{happy}(x))]$$ I am having trouble understanding whether $x$ and $y$...
151 views

### First Order Logic : Predicates

I have a small problem with the first order logic, in particular, predicate logic Let us take this sentence as an example: ...
21 views

### Can Description Logic be expressed by compiler type systems?

The Semantic Web defines standardised logic under the OWL DL standard. Programming languages such as OCamel and TypeScript support type inference and algebraic types. What are the difference between ...
42 views

### predicate logic proof of 2 numbers

For any two different numbers there is an number in between. I'm trying to write this in predicate logic and have no idea how to do it, since I need 2 variables X and Y? For all x there exists a y ...
74 views

### predicate logic/binary relation help

(1) āx, y, z (x < y ā§ y < z ā x < z) (transitivity) (2) āx Ā¬(x < x) (antisymmetry) (3) āx, y (x < y āØ x = y āØ y < x) (linearity) I need to give an example of a (nonempty) ...
66 views

383 views

### Proving that a sentence in first-order logic is not valid

By the completeness of FOL, one can show that a sentence $S$ in FOL is valid, i.e. that it holds true in every model, by exhibiting a proof of $S$. Such a proof string is a certificate of the validity ...
137 views

### Why k- Vertex Cover is not in PTIME when it can be expressed in FO-logic

We can express property that graph has vertex cover of size at most k with first order formula: \exists x_1 \exists x_2...\exists x_k (\forall y \forall z (E(z,y) \ \rightarrow \ \bigvee_{1 \leq i \...
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 ...