Problem is Variables can potentially take on an infinite number of possible values from their domains
2
Godel's Completeness Theorem
Gödel‘s completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic . It was first proven by Kurt Gödel in 1929,
Robinson
27
Resolution Principle & Herbrand Theorem
P.122(55)
28
End
29
3
Introduction
1908-1931
Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Herbrand's theorem has been extended to arbitrary higher-order logics by using expansion-tree proofs.
S C’ C S H
D S H S H
S
18
Semantic Tree
19
Semantic Tree
(P34)
H
S
20
N0
P(a) ~P(a)
N11
Q(a) ~Q(a)
N12
Q(a) ~Q(a)
N21
P(f(a)) ~P(f(a))
N24
N31
N38
P(x)
Q(x) P(f(y))
Q(f(y))}
5
Herbrand’s Theorem
The importance of Herbrand interpretations is that, if any interpretation satisfies a given set of clauses S then there is a Herbrand interpretation that satisfies them. Moreover, Herbrand's theorem states that if S is unsatisfiable then there is a finite unsatisfiable set of ground instances from the Herbrand universe defined by S. Since this set is finite, its unsatisfiability can be verified in finite time. However there may be an infinite number of such sets to check.
N3,8
N4,1
N4,2
P(x)
Q(x) P(f(y))
Q(f(y))}
24
Theorem
Herbrand Theorem
1. S S
2. S
S
25
Conclusion
Herbrand Theorem
Herbrand Theorem
26
Problem
Herbrand Theorem 30
1965
Godel's Completeness Theorem says that FOL entailment is only semidecidable
If a sentence is true given a set of axioms, there is a procedure that will determine this If the sentence is false, then there is no guarantee that a procedure will ever determine this—i.e., it may never halt
A = { P(a), Q(a, a), R(a), P(b), Q(b, a), Q(b, b), Q(a, b), R(b), P( f(a,b)), Q(f(a, b), f(a, b)), R(f(a, b), P(f(a,a)), P(f(b,a)), P(f(b,b)),……) S H
14
Herbrand Interpretation
15
Herbrand Interpretation
I H S G H D H
16
Herbrand Interpretation (cont.)
1 I S 2 S 3 S S
17
D S|I = T
I H S|I* = T S H
I*
H
I
Herbrand Interpretation (cont.)
6
Terms
Herbrand domain (H domain) Herbrand universe (H universe) Herbrand interpretation (H interpretation ) Semantic tree
7
H Domain
8
Herbrand Universe
“On Formally Undecidable Propositions of Principia Mathematica and Related Systems”
If the system is consistent, it cannot be complete. The consistency of the axioms cannot be proven within the system.
9
Herbrand Domain
D
H
Hi
Hi
1
{ f (t1 ,...,tn )}
10
D H
H
D
11
Example of H Domain
S = { P(x), Q(y,f(z,b)),R(a)} H H0 {a, b} H1 {a, b, f(a,b), f(a,a), f(b,a), f(b,b)} H2 { a, b, f(a,b), f(a,a), f(b,a), f(b,b) f(a,f(a,b)), f(a,f(a,a)), f(a, f(b,a)), f(a, f(b,b)), f(b,f(a,b)), f(b,f(a,a)), f(b, f(b,a)), f(b,f(b,b)), f(f(a,b),f(a,b)), f(f(a,b),f(a,a)), f(f(a,b), f(b,a)), f(f(a,b), f(b,b)), f(f(a,a),f(a,b)), f(f(a,a),f(a,a)), f(f(a,a), f(b,a)), f(f(a,a), f(b,b)), f(f(b,a),f(a,b)), f(f(b,a),f(a,a)), f(f(b,a), f(b,a)), f(f(b,a), f(b,b)), f(f(b,b),f(a,b)), f(f(b,b),f(a,a)), f(f(b,b), f(b,a)), f(f(b,b), f(b,b))} ……… H = H1 H2 H3………
In mathematical logic, for any formal language with a set of symbols (constants and functional symbols), the Herbrand universe recursively defines the set of all terms that can be composed by applying functional composition from the basic symbols.
Chapter 3 – part II Herbrand Theorem
Root of solution Principle
1
Problem
In the first-order logic, if the satisfiability or unsatisfiability of a sentence could be proved in finite time?
12
Herbrand Domain
f tn symbol f S t1, t2, …tn S H A } S A
13
functional constants H
Herbrand universe set A={ H H Ground term P(t1, t2, …tn) S
Example of H Universe Set
4
Herbrand’s idea
Definition Tautology ( ) true under any possible interpretation. That mean if a sentence G is Tautology, for all interpretations, G is true under it Idea Try to prove there is no interpretation in which G is true. The number of interpretations should be countable and finite