Transcript Vampire

Vampire:
A Theorem Prover for FirstOrder Classical Logic
Jason Gruber
COSC 481-1
Tuesday May 3, 2005
What is Vampire?
• developed by Andrei Voronkov and Alexandre
Riazanov
– Computer Science Department, University of
Manchester
• The main goals of the project are:
– creating an experimental environment for developing
and evaluating novel efficient implementation
techniques for automated theorem proving in firstorder logic
– developing software whose efficiency can meet
practical needs in automatic theorem proving
arising in a number of areas such as formal
verification and development of software and
hardware
2
Vampire
• At the moment our system Vampire is
– a relatively fast resolution- and superpositionbased experimental system
– a developing system; many ideas are waiting
to be implemented
• Vampire is not
– an example of good design and coding
style, though the situation is improving
3
Vampire
• It solves problems in the Thousands of Problems for
Theorem Prover syntax in both CNF (conjunctive normal
form) and full first-order logic syntax.
• Vampire supports the following inference rules:
– ordered binary resolution with negative selection
– superposition
– special form of splitting
• Vampire exploits a number of redundancy control and
simplification techniques, such as
–
–
–
–
forward and backward subsumption
forward and backward demodulation
forward subsumption resolution
cheap variant of basicness restrictions
4
Vampire
• Its kernel implements the calculi of ordered binary resolution and
Quick Facts about: superposition
(geometry) the placement of one object ideally in the position of
another one in order to show that the two coincidesuperposition for
handling equality. The splitting rule and negative equality splitting
are simulated by the introduction of new predicate definitions and
dynamic folding of such definitions. A number of standard
redundancy criteria and simplification techniques are used for
pruning the search space: subsumption, tautology deletion
(optionally modulo commutativity), subsumption resolution, rewriting
by ordered unit equalities, basicness restrictions and irreducibility of
substitution terms.
The reduction orderings used are the standard Knuth-Bendix
ordering and a special non-recursive version of the Knuth-Bendix
ordering.
5
Vampire
• A number of efficient indexing techniques are used to
implement all major operations on sets of terms and
clauses. Run-time algorithm specialization is used to
accelerate some costly operations, e.g., checks of
ordering constraints.
Although the kernel of the system works only with
clausal normal forms, the preprocessor component
accepts a problem in the full first-order logic syntax,
clausifies it and performs a number of useful
transformations before passing the result to the kernel.
When a theorem is proven, the system produces a
verifiable proof, which validates both the classification
phase and the refutation of the CNF.
6
Vampire
• The efficiency of Vampire is due to a
combination of compilation and indexing
techniques used to implement all costly
operations
• code trees are used for forward subsumption
and search for generalizations, combination of
path indexing and database style joins for
backward subsumption and demodulation, and a
number of specialized versions of discrimination
trees for resolution and superposition.
7
Vampire
• Another interesting feature, which makes
the system competitive, is the so-called
limited resource strategy (LRS)* . Its
purpose is to provide the best
performance when time is limited by
minimizing the amount of work that has
been wasted when the time limit
is reached.
8
Trophies
• CASC-16 (1999) : 1st place in MIX
CASC-17 (2000) : 1st place in FOF (combined with
Flotter)
CASC JC (2001) : 1st place in MIX Proof Class and joint
1st place with E-SETHEO in MIX Assurance Class
CASC-18 (2002) : 1st place in MIX (both Proof Class
and Assurance Class), 1st place in FOF
CASC-19 (2003) : 1st place in MIX (v6.0, both Proof
Class and Assurance Class), 1st place in FOF (v5.0)
CASC-J2 (2004) : 1st place in MIX (both Proof Class
and Assurance Class), 1st place in FOF
9
Related work (incomplete list)
• The kernel of Vampire is used in a new
temporal prover TeMP
• Vampire is integrated into the Sigma
knowledge engineering environment.
• Vampire is used in the Hoolet reasoner
for OWL-DL
• Vampire is being integrated into Isabelle
10
First Order Logic
An overview
Syntax of First Order Logic
12
Semantics for First Order Logic
13
First Order Logic
• First order logic is used to model the
world in terms of:
–
–
–
–
Objects, which are things with individual identities
Properties of objects that distinguish them from other objects
Relations that hold among objects
Functions which are a subset of the relations in which there is only one
‘value’ for any given ‘input’
• Examples:
– Objects: Students, lectures, companies, cars…
– Relations: Brother of, bigger than, outside, part of, has color, occurs
after, owns, visits, precedes…
– Properties: blue, oval, even, large
– Functions: father of, best friend, second half, one more than…
14
User Provides
• Constant symbols which represent individuals
in the world
– Mary
–3
– green
• Function symbols which map individuals to
individuals
– Father-of(Mary)=John
– Color-of(Sky)=Blue
• Predicate symbols mapping from individuals to
truth values
– Greater(5,3)
– Green(Grass)
– Color(Grass, Green)
15
FOL Provides
• Variable symbols
– E.g., x, y, foo
• Connectives
– Same as in PL; not (¬), and (), or (), implies
(), if and only if ()
• Quantifiers
– Universal "x
– Existential x
16
Quantifiers
• Universal quantification
– ("x)P(x) means that P holds for all values of x
in the domain associated with that variable
• E.g., ("x) dolphin(x)mammal(x)
• Existential quantification
– (x)P(x) means that P holds for some value of
x in the domain associated with that variable
– E.g., (x)mammal(x)lays-eggs(x)
– Make a statement about some object without
naming it
17
Sentences are built from terms
and atoms
• A term (denoting a real-world individual) is a constant symbol, a
variable symbol, or an n-place function of n terms.
– X and f(x1,…,xn) are terms, where each xi is a term. A term with no
variables is a Ground Term
• An atom (which has value true or false) is either
– An n-place predicate of n terms, or,
– ¬P, PQ, PQ, PQ, PQ where P and Q are atoms
• A sentence is an atom, or, if P is a sentence and x is a variable, then
("x)P and (x)P are sentences.
• A well-formed formula (wff) is a sentence containing no “free”
variables, IE, all variables are ‘bound’ by universal or existential
quantifiers.
– ("x)P(x,y) has x bound as a universally quantified variable, but y is free
18
Translating English to FOL
• Every gardener likes the sun
– ("x) gardener(x)likes(x,sun)
• You can fool some of the people all of the time.
– (x)("t)(person(x)time(t))can-fool(x,t)
• You can fool all of the people some of the time.
– ("x)(t)(person(x)time(t))can-fool(x,t)
• All purple mushrooms are poisonous.
– ("x)(mushroom(x)purple(x))poisonous(x)
• No purple mushroom is poisonous.
– ¬(x)purple(x)mushroom(x)poisonous(x)
– ("x)(mushroom(x)purple(x))¬poisonous(x)
• There are exactly two purple mushrooms.
– (x)(y)mushroom(x)purple(x)mushroom(y)purple(y)¬(x=y)(Az)(
mushroom(z)purple(z))((x=z)v)y=z))
• Clinton is not tall.
– ¬tall(Clinton)
• X is above Y if X is directly on top of Y or there is a pile of one or
more other objects directly on top of another starting with X and
ending with Y.
– ("x)("y)above(x,y)(on(x,y)v(z)(on(x.z)above(z,y)))
19
Quantifiers
• Universal quantifiers often used with “implies” to form “rules.”
– ("x) student(x)smart(x) means “all students are smart.”
• You rarely use universal quantification to make blanket statements
about every individual in the world.
– ("x)student(x)smart(x) means everyone in the world is a student and
is smart.
• Existential quantifiers usually used with “and” to specify a list of
properties about an individual.
– (x)student(x)smart(x) means “there is a student who is smart.”
• A common mistake is to represent this English sentence as the FOL
sentence:
– (x)student(x)smart(x)
• But what happens when there is a person who is NOT a student?
20
Connections between All & Exist
• We can relate sentences involving for all
and exists with DeMorgan’s Laws:
–
–
–
–
("x) ¬P  ¬(x) P
¬("x) P  (x) ¬ P
("x) P  ¬(x) ¬ P
(x) P  ¬("x) ¬ P
21
Axioms, definitions and
theorems
• Axioms are facts and rules which attempt to capture all of the
(important) facts and concepts about a domain that can be used to
prove theorems.
– Mathematicians don’t want any unnecessary (dependent) axioms—ones that can
be derived from other axioms.
– Dependent axioms can make reasoning faster, however.
– Choosing a good set of axioms for a domain is a kind of design problem.
• A definition of a predicate is of the form “p(X)  …” and can be
decomposed into two parts
– Necessary description: “p(x)  …”
– Sufficient description: “p(x)…”
– Some concepts do not have complete definitions (e.g. person(x))
22
Conversion to Normal Form
• STEP 1 - Eliminate implications:
– The first step is to convert all implications with
corresponding disjunctions.
– ie. p  q becomes ¬ p  q
• STEP 2 - Move  inwards:
– Use de Morgan’s laws, quantifier equivalences, and
double negations
– ¬(p  q) becomes ¬ p  ¬ q
¬(p  q) becomes ¬ p  ¬ q
¬ " x, p becomes x ¬ p
¬  x, p becomes "x ¬ p
¬ ¬ p becomes p
23
Steps 3 & 4
• STEP 3 - Standardize variables:
– Change all duplicate variable names to
separate names to Avoid confusion later when
we drop quantifiers
• ("x P(x))  (x Q(x)) becomes ("x P(x))  (y Q(y))
• STEP 4 - Move quantifiers left:
– This can be done because we removed all
duplicate variables
• p  "x q becomes "x p  q
24
Steps 5-8
• STEP 5 - Skolemize:
– Remove all existential quantifiers Replace variables with names
not existing elsewhere in KB
• Simple case: x Q(x) becomes Q(A) where A is unique
• STEP 6 - Distribute  over :
– (a  b)  c becomes (a  c)  (b  c)
• STEP 7 - Flatten nested conjunctions and
disjunctions:
– (a  b)  c becomes (a  b  c) (a  b)  c becomes (a  b  c)
• STEP 8 - Convert disjunctions to implications:
– Optional step for converting to INF
– Gather all negative literals to left, and positive literals to right
• ( a   b  c  d) becomes (a  b  c  d)
25
English & FOL example
• Russell and Norvig Example
26
Now we apply the conversion
procedure
27
28
References
• http://www.absoluteastronomy.com/encyclopedia/V/Va/V
ampire_theorem_prover.htm
• http://www.cs.man.ac.uk/~riazanoa/Vampire/
• www.doc.ic.ac.uk/~sgc/teaching/v231/lecture9.ppt
• http://www.rci.rutgers.edu/~cfs/305_html/Deduction/FOL.
html
• http://sern.ucalgary.ca/courses/CPSC/533/W99/presenta
tions/L2_9B_Kolackowsky_Sit/
• http://www.csee.umbc.edu/471/lectures/7/sld001.htm
•
A.Riazanov,A.Voronkov, Limited Resource Strategy in Resolution Theorem
Proving, Preprint CSPP-7, University of Manchester, 2000
29