Chapter 5: First-Order Logic

5.1 Introduction¶

First-order logic (FOL), also called predicate logic, is a more powerful extension of propositional logic that enables complex reasoning about objects and their relationships—essential for real-world AI applications like expert systems.

Why First-Order Logic?¶

Limitations of Propositional Logic:

Propositional logic cannot express general statements about classes of objects. Consider:

• “All mammals give birth to live babies”

• “A cat is a mammal”

• Therefore: “A cat gives birth to live babies”

In propositional logic, you would need separate rules for every mammal (cat, dog, elephant, etc.), making knowledge bases unwieldy or impossible when dealing with large or infinite domains.

What First-Order Logic Provides:

1. Objects: Represent entities in the domain (people, movies, awards)

2. Relations: Express relationships between objects

3. Functions: Map objects to other objects

4. Quantifiers: Make statements about all or some objects

5. Variables: Bind to any object in a domain

Real-World Applications:

• Expert systems (medical diagnosis, legal reasoning)

• Natural language understanding

• Semantic web and knowledge graphs

• Database query languages (SQL is based on FOL)

• Automated theorem proving

• Planning and scheduling systems

5.2 Syntax of First-Order Logic¶

5.2.1 Basic Components¶

Constants - Represent specific objects:

• Examples: $\text{John}, \text{Mary}, \text{Beef}, \text{StevenSpielberg}$

Variables - Represent arbitrary objects from a domain:

• Denoted: $x, y, z, ...$

• Must be bound by quantifiers or substitution

Functions - Map objects to objects:

• $\text{Father}(x)$: the father of $x$

• $\text{Fav}(x)$: favorite food of person $x$

• Arity: number of arguments (e.g., $\text{Father}$ has arity 1)

Predicates - Functions that return truth values:

• $E(x, y)$: person $x$ eats food $y$

• $F(x, y, z)$: director $x$ won award $z$ for movie $y$

• Arity: number of arguments

Example:

This predicate is true when Steven Spielberg won Best Director for Saving Private Ryan.

5.2.2 Terms¶

A term represents an object and can be:

1. A constant: $\text{John}$

2. A variable: $x$

3. A function applied to terms: $\text{Father}(\text{John})$, $\text{Fav}(x)$

Examples of terms:

• $\text{John}$ ✓

• $\text{Father}(\text{Mary})$ ✓

• $\text{Father}(\text{Father}(x))$ ✓ (grandfather of $x$)

5.2.3 Atomic Formulas¶

An atomic formula (atom) is formed by applying a predicate to terms:

where $P$ is a predicate and $t_i$ are terms.

Examples:

• $E(\text{John}, \text{Beef})$ - John eats beef

• $N(x)$ - $x$ is non-vegetarian

• $A(x, y)$ - $x$ is an ancestor of $y$

5.2.4 Logical Operators¶

FOL uses the same operators as propositional logic:

5.2.5 Complex Formulas¶

Complex formulas are built recursively:

1. Every atomic formula is a formula

2. If $\alpha$ is a formula, then $\neg \alpha$ is a formula

3. If $\alpha$ and $\beta$ are formulas, then:

   • $(\alpha \land \beta)$, $(\alpha \lor \beta)$, $(\alpha \rightarrow \beta)$, $(\alpha \leftrightarrow \beta)$ are formulas

4. Quantified formulas (see next section)

5.3 Quantifiers¶

Quantifiers allow statements about entire domains or existence of objects.

5.3.1 Universal Quantifier ($\forall$)¶

The universal quantifier $\forall x$ means “for all $x$” or “for every $x$”.

Syntax: $\forall x \, \alpha$

Meaning: Formula $\alpha$ is true for every object $x$ in the domain.

Examples:

1. Everyone who eats beef is non-vegetarian:

   $$\forall x \, [E(x, \text{Beef}) \rightarrow N(x)]$$

   (3)

2. All mammals give birth to live babies:

   $$\forall x \, [\text{Mammal}(x) \rightarrow \text{LiveBirth}(x)]$$

   (4)

3. Award winners are invited to the Oscars:

   $$\forall x, y, z \, [F(x, y, z) \rightarrow O(x)]$$

   (5)

Connection to conjunction: Universal quantification over a finite domain $\{a, b, c\}$ is equivalent to conjunction:

5.3.2 Existential Quantifier ($\exists$)¶

The existential quantifier $\exists x$ means “there exists an $x$” or “for some $x$”.

Syntax: $\exists x \, \alpha$

Meaning: Formula $\alpha$ is true for at least one object $x$ in the domain.

Examples:

1. Someone eats beef:

   $$\exists x \, E(x, \text{Beef})$$

   (7)

2. There is a non-vegetarian person who eats beef:

   $$\exists x \, [N(x) \land E(x, \text{Beef})]$$

   (8)

   Note: $\exists x \, [N(x) \rightarrow E(x, \text{Beef})]$ is wrong - it’s true whenever there’s a vegetarian!

3. Everyone eats something:

   $$\forall x \, \exists y \, E(x, y)$$

   (9)

Connection to disjunction: Existential quantification over a finite domain $\{a, b, c\}$ is equivalent to disjunction:

5.3.3 Quantifier Order Matters¶

The order of quantifiers changes meaning dramatically:

Example 1: Everyone eats something (possibly different for each person)

Example 2: There’s one special food everyone eats

The second is much stronger and likely false!

General Rule:

• $\forall x \, \forall y \, \alpha \equiv \forall y \, \forall x \, \alpha$ (order doesn’t matter for same quantifier)

• $\exists x \, \exists y \, \alpha \equiv \exists y \, \exists x \, \alpha$

• But $\forall x \, \exists y \, \alpha \not\equiv \exists y \, \forall x \, \alpha$ (order matters for mixed quantifiers!)

5.3.4 Scope and Bound Variables¶

The scope of a quantifier is the formula it applies to (usually in brackets).

A variable is bound if it appears within the scope of a quantifier for that variable.

A variable is free if it’s not bound by any quantifier.

Example:

Here, $x$ is bound, but $y$ is free.

Closed formulas (sentences) have no free variables - these are what knowledge bases contain.

5.3.5 Standardization¶

Standardization uses different variable names for different quantifiers to avoid confusion.

Bad (confusing):

The second $x$ is free!

Good (standardized):

Or better yet:

5.4 Semantics of First-Order Logic¶

5.4.1 Interpretations¶

An interpretation (or model) specifies:

1. Domain: A non-empty set of objects

2. Constant assignments: Each constant denotes a specific object

3. Function assignments: Each function maps objects to objects

4. Predicate assignments: Each predicate has a truth value for each combination of objects

Example: For a knowledge base about people and food:

• Domain: $\{\text{John}, \text{Mary}, \text{Beef}, \text{Carrots}\}$

• $E(\text{John}, \text{Beef}) = \text{True}$

• $E(\text{Mary}, \text{Carrots}) = \text{True}$

• $N(\text{John}) = \text{True}$

• $N(\text{Mary}) = \text{False}$

5.4.2 Truth in a Model¶

A formula is true in a model (satisfied) if:

For atomic formulas: Check the predicate assignment

For negation: $\neg \alpha$ is true iff $\alpha$ is false

For connectives: Use truth tables as in propositional logic

For $\forall x \, \alpha$: True iff $\alpha$ is true for every object in the domain

For $\exists x \, \alpha$: True iff $\alpha$ is true for at least one object in the domain

5.4.3 Validity and Satisfiability¶

A formula is valid (tautology) if it’s true in all possible models.

Example: $\forall x \, [P(x) \lor \neg P(x)]$ is valid.

A formula is satisfiable if it’s true in at least one model.

A formula is unsatisfiable (contradiction) if it’s false in all models.

Example: $\exists x \, [P(x) \land \neg P(x)]$ is unsatisfiable.

5.4.4 Entailment¶

$KB \models \alpha$ means $KB$ entails $\alpha$: in every model where $KB$ is true, $\alpha$ is also true.

Entailment via unsatisfiability:

This is the basis for proof by contradiction in FOL.

5.5 Quantifier Manipulation Laws¶

5.5.1 Negation and Quantifiers¶

De Morgan’s Laws for Quantifiers:

Key insight: Pushing negation through a quantifier flips its type.

Example:

• “Not everyone is non-vegetarian” = “Someone is vegetarian”

• $\neg (\forall x \, N(x)) \equiv \exists x \, \neg N(x)$

Justification: For finite domain $\{a, b, c\}$:

5.5.2 Operator Precedence¶

From highest to lowest precedence:

1. Quantifiers: $\forall, \exists$

2. Negation: $\neg$

3. Conjunction: $\land$

4. Disjunction: $\lor$

5. Implication: $\rightarrow$

6. Biconditional: $\leftrightarrow$

Example:

means $(\forall x \, P(x)) \land Q(x)$ (quantifier has highest precedence)

To quantify the full expression, use brackets:

5.6 Unification and Substitution¶

5.6.1 Substitution¶

Substitution replaces variables with terms.

Notation: $\{x/t\}$ means replace $x$ with term $t$

Example:

5.6.2 Types of Substitution¶

Ground Substitution: Replace variable with a constant

From $\forall x \, [E(x, \text{Beef}) \rightarrow N(x)]$, we can infer:

Flat Substitution: Replace one variable with another

From $\forall x \, P(x)$, we can infer $\forall y \, P(y)$ (just renaming)

5.6.3 Unification¶

Unification finds a substitution that makes two expressions identical.

Definition: A substitution $\theta$ unifies expressions $E_1$ and $E_2$ if $E_1\theta = E_2\theta$

Examples:

1. Unify $P(x)$ and $P(a)$:

   • Substitution: $\theta = \{x/a\}$

   • Result: $P(a)$

2. Unify $P(x, f(y))$ and $P(a, f(b))$:

   • Substitution: $\theta = \{x/a, y/b\}$

   • Result: $P(a, f(b))$

3. Unify $P(x, x)$ and $P(a, b)$:

   • Cannot unify - would require $x = a$ and $x = b$ simultaneously

4. Unify $P(x, f(y))$ and $P(y, f(a))$:

   • Substitution: $\theta = \{x/a, y/a\}$

   • Result: $P(a, f(a))$

5.6.4 Most General Unifier (MGU)¶

Among all possible unifiers, the most general unifier (MGU) is preferred.

Example: Unify $P(x)$ and $P(y)$

• Possible: $\{x/a, y/a\}$ giving $P(a)$

• Possible: $\{x/b, y/b\}$ giving $P(b)$

• MGU: $\{x/y\}$ or $\{y/x\}$ giving $P(y)$ or $P(x)$

The MGU is most general because it can be specialized further.

5.6.5 Unification Algorithm¶

Algorithm: UNIFY(E1, E2)

begin
    θ ← {}  // Empty substitution
    
    if E1 and E2 are identical then
        return θ
    
    if E1 is a variable then
        if E1 occurs in E2 then
            return FAIL  // Occur check
        else
            return {E1/E2}
    
    if E2 is a variable then
        return UNIFY(E2, E1)
    
    if E1 = f(E1_1, ..., E1_n) and E2 = g(E2_1, ..., E2_m) then
        if f ≠ g or n ≠ m then
            return FAIL
        
        θ ← {}
        for i = 1 to n do
            θ_i ← UNIFY(E1_iθ, E2_iθ)
            if θ_i = FAIL then
                return FAIL
            θ ← θ ∪ θ_i
        
        return θ
end

Complexity: $O(n^2)$ where $n$ is the size of expressions

Occur check: Prevents infinite structures like $x = f(x)$

5.7 Inference in First-Order Logic¶

5.7.1 Generalized Modus Ponens¶

Classical Modus Ponens from propositional logic:

In FOL, we need Generalized Modus Ponens with unification:

Given:
  1. Rule: ∀x [P(x) → Q(x)]
  2. Fact: P(a)
  
Steps:
  1. Instantiate rule with x/a: P(a) → Q(a)
  2. Apply Modus Ponens: Q(a)

More generally:

where $\theta$ unifies each $P_i'$ with $P_i$

Example:

Given:

• Rule: $\forall x, y \, [E(x, y) \land M(y) \rightarrow N(x)]$ (eating meat makes you non-vegetarian)

• Facts: $E(\text{John}, \text{Beef})$ and $M(\text{Beef})$

Steps:

1. Unify $E(x, y)$ with $E(\text{John}, \text{Beef})$: $\theta_1 = \{x/\text{John}, y/\text{Beef}\}$

2. Check $M(\text{Beef})$ holds: ✓

3. Apply substitution to conclusion: $N(\text{John})$

5.7.2 Universal Instantiation¶

From a universally quantified statement, infer any instance:

where $t$ is any ground term

Example:

5.7.3 Existential Instantiation¶

From an existentially quantified statement, introduce a new constant (Skolem constant):

where $c$ is a new constant (Skolem constant) not appearing elsewhere

Example:

Here, “John” is a Skolem constant representing “some king”.

5.7.4 Skolemization¶

Purpose: Eliminate existential quantifiers to simplify inference.

Skolem Constants (when $\exists$ is not in scope of $\forall$):

where $c$ is a new Skolem constant

Skolem Functions (when $\exists$ is in scope of $\forall$):

Here $f(x)$ is a Skolem function: the food that person $x$ eats depends on $x$.

Complex Example:

Original:

After Skolemization:

• $f(x)$ depends only on $x$ (outer $\forall$)

• $g(x, z)$ depends on both $x$ and $z$ (both $\forall$ in its scope)

5.8 Forward and Backward Chaining¶

5.8.1 First-Order Definite Clauses¶

A first-order definite clause has the form:

• Antecedent: conjunction of positive literals

• Consequent: single positive literal

• Variables are universally quantified (implicit)

Examples:

• $\text{Parent}(x, y) \rightarrow \text{Ancestor}(x, y)$

• $\text{Parent}(x, z) \land \text{Ancestor}(z, y) \rightarrow \text{Ancestor}(x, y)$

• $\text{Cat}(x) \rightarrow \text{Mammal}(x)$

Facts are definite clauses with empty antecedent:

• $\text{Parent}(\text{John}, \text{Mary})$

• $\text{Cat}(\text{Whiskers})$

5.8.2 Forward Chaining Algorithm¶

Forward chaining is data-driven: start with known facts, derive new facts until query is reached.

Algorithm: FOL-FC-ASK(KB, query)

begin
    facts ← all ground atomic sentences in KB
    
    repeat
        new ← {}
        
        for each rule r in KB do
            for each substitution θ that unifies premises of r with facts do
                conclusion ← (head of r)θ
                
                if conclusion = query then
                    return True
                
                if conclusion not in facts then
                    new ← new ∪ {conclusion}
        
        if new = {} then
            return False  // No new facts derived
        
        facts ← facts ∪ new
    
    until False
end

Properties:

• Sound: Only derives true consequences

• Complete: For definite clauses, will find all entailed facts

• Datalog complexity: Polynomial in KB size (for function-free Horn clauses)

Example: Prove $\text{Ancestor}(\text{John}, \text{Mary})$

Given:

• Facts: $\text{Parent}(\text{John}, \text{Bob})$, $\text{Parent}(\text{Bob}, \text{Mary})$

• Rules:

  1. $\text{Parent}(x, y) \rightarrow \text{Ancestor}(x, y)$

  2. $\text{Parent}(x, z) \land \text{Ancestor}(z, y) \rightarrow \text{Ancestor}(x, y)$

Iteration 1:

• Apply rule 1 with $\{x/\text{John}, y/\text{Bob}\}$: infer $\text{Ancestor}(\text{John}, \text{Bob})$

• Apply rule 1 with $\{x/\text{Bob}, y/\text{Mary}\}$: infer $\text{Ancestor}(\text{Bob}, \text{Mary})$

Iteration 2:

• Apply rule 2 with $\{x/\text{John}, z/\text{Bob}, y/\text{Mary}\}$: infer $\text{Ancestor}(\text{John}, \text{Mary})$ ✓

5.8.3 Backward Chaining Algorithm¶

Backward chaining is goal-driven: start with query, work backward to find supporting facts.

Algorithm: FOL-BC-ASK(KB, goal)

begin
    if goal is a known fact in KB then
        return True
    
    for each rule r in KB where head unifies with goal do
        θ ← UNIFY(head of r, goal)
        premises ← (body of r)θ
        
        if FOL-BC-ASK-ALL(KB, premises) then
            return True
    
    return False
end

Algorithm: FOL-BC-ASK-ALL(KB, premises)

begin
    if premises is empty then
        return True
    
    first ← first premise in premises
    rest ← remaining premises
    
    for each substitution θ that makes FOL-BC-ASK(KB, first) = True do
        if FOL-BC-ASK-ALL(KB, restθ) then
            return True
    
    return False
end

Properties:

• Sound: Only returns True if entailment holds

• Complete: For definite clauses

• Efficient: Only explores relevant parts of KB

• Depth-first: Can loop infinitely (needs cycle detection)

Example: Same as forward chaining, but working backward from $\text{Ancestor}(\text{John}, \text{Mary})$

5.8.4 Forward vs Backward Chaining¶

5.9 Resolution in First-Order Logic¶

Resolution is the most powerful inference method for FOL, generalizing propositional resolution.

5.9.1 Conversion to CNF¶

To use resolution, first convert $KB \land \neg \alpha$ to CNF:

Steps:

1. Eliminate implications and biconditionals

   • $P \rightarrow Q \Rightarrow \neg P \lor Q$

   • $P \leftrightarrow Q \Rightarrow (\neg P \lor Q) \land (\neg Q \lor P)$

2. Move negation inward (De Morgan + quantifiers)

   • $\neg(P \land Q) \Rightarrow \neg P \lor \neg Q$

   • $\neg(P \lor Q) \Rightarrow \neg P \land \neg Q$

   • $\neg \forall x \, P(x) \Rightarrow \exists x \, \neg P(x)$

   • $\neg \exists x \, P(x) \Rightarrow \forall x \, \neg P(x)$

3. Standardize variables (different names for different quantifiers)

4. Skolemize (eliminate $\exists$)

   • Replace existential variables with Skolem functions

5. Drop universal quantifiers (all remaining variables are $\forall$)

6. Distribute $\lor$ over $\land$

   • $P \lor (Q \land R) \Rightarrow (P \lor Q) \land (P \lor R)$

Example: Convert to CNF

Original:

Step 1 (eliminate $\rightarrow$):

Step 4 (Skolemize $\exists y$ inside $\forall x$):

Step 5 (drop $\forall$):

This is now in CNF.

5.9.2 Resolution Rule with Unification¶

Propositional resolution:

First-order resolution (with unification):

where $\theta = \text{UNIFY}(\ell_1, \neg m_1)$

Example:

Clauses:

1. $\neg \text{Cat}(x) \lor \text{Mammal}(x)$

2. $\text{Cat}(\text{Whiskers})$

Resolution:

• Unify $\text{Cat}(x)$ with $\text{Cat}(\text{Whiskers})$: $\theta = \{x/\text{Whiskers}\}$

• Resolve: $\text{Mammal}(\text{Whiskers})$

5.9.3 Resolution Algorithm¶

Algorithm: FOL-RESOLUTION(KB, α)

begin
    clauses ← CNF(KB ∧ ¬α)
    new ← {}
    
    loop
        for each pair (Ci, Cj) of clauses in clauses do
            resolvents ← RESOLVE(Ci, Cj)
            
            if resolvents contains empty clause □ then
                return True  // Proved by contradiction
            
            new ← new ∪ resolvents
        
        if new ⊆ clauses then
            return False  // No progress, cannot prove
        
        clauses ← clauses ∪ new
end

Algorithm: RESOLVE(Ci, Cj)

begin
    resolvents ← {}
    
    for each literal ℓi in Ci do
        for each literal ℓj in Cj do
            if θ = UNIFY(ℓi, ¬ℓj) exists then
                resolvent ← ((Ci - {ℓi}) ∪ (Cj - {ℓj}))θ
                resolvents ← resolvents ∪ {resolvent}
    
    return resolvents
end

Properties:

• Sound: Only derives true conclusions

• Refutation-complete: Can prove any entailed sentence by finding contradiction

• Semi-decidable: May not terminate for non-entailed sentences

Complete Example:

Prove: All cats are mammals; Whiskers is a cat; therefore Whiskers is a mammal.

KB:

1. $\forall x \, [\text{Cat}(x) \rightarrow \text{Mammal}(x)]$

2. $\text{Cat}(\text{Whiskers})$

Query: $\text{Mammal}(\text{Whiskers})$

CNF of $KB \land \neg \text{Mammal}(\text{Whiskers})$:

1. $\neg \text{Cat}(x) \lor \text{Mammal}(x)$

2. $\text{Cat}(\text{Whiskers})$

3. $\neg \text{Mammal}(\text{Whiskers})$

Resolution steps:

• Resolve (1) and (2) with $\{x/\text{Whiskers}\}$: $\text{Mammal}(\text{Whiskers})$

• Resolve $\text{Mammal}(\text{Whiskers})$ and (3): $\square$ (empty clause)

Contradiction found → $KB \models \text{Mammal}(\text{Whiskers})$ ✓

5.10 Practical Knowledge Engineering¶

5.10.1 Designing a Knowledge Base¶

Steps:

1. Identify the domain: What objects and relationships exist?

2. Choose vocabulary:

   • Constants for objects

   • Predicates for properties and relations

   • Functions for mappings

3. Encode general knowledge: Universal rules

4. Encode specific facts: Ground instances

5. Query and test: Verify inferences are correct

5.10.2 Example: Family Relations¶

Domain: People and family relationships

Vocabulary:

• Constants: John, Mary, Bob, Sue

• Predicates: Parent(x,y), Male(x), Female(x)

• Functions: Father(x), Mother(x)

Rules:

Parent(x,y) ∧ Parent(y,z) → Grandparent(x,z)
Parent(x,y) ∧ Male(x) → Father(x) = x
Parent(x,y) ∧ Parent(x,z) ∧ y≠z → Sibling(y,z)
Parent(x,y) ∧ Parent(z,w) ∧ Sibling(y,w) → Cousin(x,z)

Facts:

Parent(John, Mary)
Parent(Mary, Bob)
Male(John)
Female(Mary)

Query: Is John a grandparent of Bob?

Inference: Apply first rule with appropriate substitutions → Yes!

5.10.3 Common Patterns¶

Transitive Relations:

P(x,y) → Ancestor(x,y)
P(x,z) ∧ Ancestor(z,y) → Ancestor(x,y)

Symmetric Relations:

Sibling(x,y) → Sibling(y,x)

Equivalence Classes:

SameSpecies(x,y) ∧ SameSpecies(y,z) → SameSpecies(x,z)

5.11 Summary¶

Key Concepts¶

1. Expressive Power: FOL can represent objects, relations, and quantification

2. Syntax: Constants, variables, functions, predicates, quantifiers

3. Semantics: Interpretations, models, truth values

4. Quantifiers: $\forall$ (universal), $\exists$ (existential)

5. Unification: Making expressions identical via substitution

6. Skolemization: Eliminating existential quantifiers

7. Inference: Generalized Modus Ponens, forward/backward chaining, resolution

Comparison with Propositional Logic¶

Decidability¶

First-order logic is semi-decidable:

• If $KB \models \alpha$, resolution will eventually prove it (complete)

• If $KB \not\models \alpha$, resolution may run forever (not decidable)

This contrasts with propositional logic, which is fully decidable.

Why FOL Matters¶

First-order logic is the foundation for:

• Knowledge representation: Expert systems, medical diagnosis

• Semantic web: RDF, OWL, SPARQL

• Databases: SQL query languages

• Planning: STRIPS, PDDL

• Natural language: Semantic parsing

• Theorem proving: Automated reasoning systems

5.12 Implementation¶

For complete Python implementations, see:

Chapter 5: First-Order Logic - Implementation

The implementation notebook includes:

1. Expression Classes: Variable, Constant, Function, Predicate

2. Term and Formula Structures: Atomic, compound, quantified

3. Unification Algorithm: MGU computation with occur check

4. Substitution: Ground and flat substitution operations

5. CNF Conversion: Full pipeline with Skolemization

6. Forward Chaining: FOL-FC-ASK with unification

7. Backward Chaining: FOL-BC-ASK depth-first search

8. Resolution Prover: Complete theorem proving

9. Knowledge Base: Store and query FOL sentences

10. Real-World Applications:

    • Family relationship reasoner

    • Expert system for classification

    • Natural deduction proofs

Further Reading¶

Textbooks¶

• Aggarwal, C. C. (2021). Artificial Intelligence: A Textbook. Springer. [Chapter 5]

• Russell, S., & Norvig, P. (2020). Artificial Intelligence: A Modern Approach (4th ed.). Pearson. [Chapter 8-9]

• Genesereth, M., & Nilsson, N. (1987). Logical Foundations of Artificial Intelligence. Morgan Kaufmann.

• Fitting, M. (1996). First-Order Logic and Automated Theorem Proving. Springer.

Classic Papers¶

• Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1), 23-41.

• Herbrand, J. (1930). Investigations in proof theory. From Frege to Gödel, 525-581.

• Robinson, J. A. (1965). Automatic deduction with hyper-resolution. International Journal of Computer Mathematics, 1(3), 227-234.

Automated Reasoning¶

• Chang, C. L., & Lee, R. C. T. (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press.

• Wos, L., et al. (1984). Automated Reasoning: Introduction and Applications. Prentice-Hall.

• Bundy, A. (1983). The Computer Modelling of Mathematical Reasoning. Academic Press.

Online Resources¶

• TPTP Problem Library - Thousands of FOL problems

• Prover9/Mace4 - Automated theorem prover

• Stanford Encyclopedia: Logic and AI