Mechanical Theorem Proving____ The Intellectual Excitement of Computer Science
Introduction Mechanical theorem proving is an important subject in artificial intelligence Even though Turing showed that there is no general decision procedure to check the validity of formulas of the first-order logic, there are proof procedures which can verify that a formula is valid if indeed it is valid...
Our Research Journey Journals about automated theorem proving Difficult and technical material required background we lacked Talked with professors, read about basic logic
Overview of Automated Theorem Proving Theory and history of the field -- lesson in logic Applications of automated theorem provers
Quick History and Theory Principles of Automated Theorem Proving heavily based on symbolic logic Learning the basic vocabulary and concepts was essential to understanding those principles The history of this field can be easier understood along with theories Quick lesson in symbolic logic
Different sorts of logic... Higher Order First Order Propositional
Propositional Logic A proposition is a declarative sentence that is either true or false (it cannot be both). Examples of propositions: ”Stuff at Stanford Shopping Mall is expensive", ”Elita is a bargain hunter", ”Elita is shop-aholic at Stanford mall".
Propositional Logic B Stuff at Stanford Shopping Mall is expensive C Elita is a bargain hunter D Elita is a shop-aholic at Stanford Mall Symbols, such as B, C, D, that are used to denote propositions are called atoms
Propositional Logic Example: The sentence "If stuff at Stanford Shopping mall is expensive and Elita is a bargain hunter, then Elita is not a shop-aholic at Stanford Mall" can be represented by (( B C) (D)) As we see, this compound proposition can represent a complicated idea that we deal with in everyday life.
Propositional Logic
Propositional Logic The assignment of truth values {T,F} to {G, H} is one of four interpretations of formula F (G H) Equivalent formulas Example: Suppose that bike accidents increase if there are more freshmen on campus. Also, suppose that students will start building their own impact airbags for their bikes when bike accidents increase. Assume that there are more freshmen on campus. Show that you can conclude that students will starting building their own airbags.
Propositional Logic Example... The four following statements correspond to this example: 1. If there are more freshmen on campus, the bike accidents increase 2. If bike accidents increase, students start building bike airbags 3. More freshmen on campus 4. Students will start building bike airbags
First Order Logic First order logic is a more expressive logic than propositional logic. For example, propositional logic cannot denote the following: P: Every man is mortal Q: Confucius is a man R: Confucius is mortal
First Order Logic First order logic has three more logical notions than propositional logic terms, predicates, and quantifiers Most of mathematical and everyday language can be symbolized by the first-order logic.
First Order Logic - New Terms Predicate Quantifier Interpretation -- different from propositional "An interpretation of a formula F in the first-order logic consists of a nonempty domain D, and an assignment of 'values' to each constant, function symbol, and predicate symbol occurring in F as follows: - To each constant, we assign an element in D.
- To each n-place function symbol, we assign a mapping from D^n to D.
- To each n-place predicate symbol, we assign a mapping from D^n to {T, F}."
First Order Logic - New Terms Satisfiable- A formula P is satisfiable (consistent) if and only if there exists an interpretation I such that P has a truth value of True in I. Unsatisfiable
Leibniz (1646-1716) tried to prove validity of formula Turing and Church (1936) Herbrand’s contribution Robinson’s Resolution
Resolution Herbrand’s procedure’s problem: amount of time needed to implement increase exponentially (too many interpretations to generate!) Resolution decreases the number of interpretations
Resolution The basic idea of the resolution principle is to check rather any set S of clauses contains the empty clause . If S contains , then S is unsatisfiable. If S does not contain , then check to see if can be derived from S. If it can, then it is also unsatisfiable. Example in propositional logic Example in first order logic
Propositional Resolution For propositional logic, the principle can be roughly described as the following: combine the literal that are complementary to each other so that they cancel out (e.g. P and ~P are complementary). Example in propositional logic
First Order Resolution substitution and unification Example in first order logic
First Order Resolution S = {T(x,y,u,v) v P(x,y,u,v), P(x,y,u,v) v E(x,y,v,u,v,y), T(a,b,c,d), E(a,b,d,c,d,b)} 1. T(x,y,u,v) v P(x,y,u,v) 2. P(x,y,u,v) v E(x,y,v,u,v,y) 3. T(a,b,c,d) 4. E(a,b,d,c,d,b) 5. ~P(a,b,c,d) 6.~T(a,b,c,d) 7.
Applied Theory First order specifications Boyer and Moore’s Induction
Intel Pentium Chip Specification - IEEE level 74 “when rounding towards negative infinity, the result shall be the format’s value ... closest to and no greater than the infinitely precise result”
Intel Pentium Chip Specification - IEEE level 74 round(toNegInf, R, V) = (R <= V) ^ (V < R + ulp+) R = result, V = value to be rounded,
Induction Algorithm
Applications Mathematical proof checking The QED Project Computer chip verifications Software verification
Mathematical Proof Checking Automated theorem provers do not “automate” math “Debugs” proofs Hard to use many proof checkers
The QED Project Effort of scientists from many laboratories and institutions
Reduce mathematical “noise pollution.” Speed publication of papers by taking focus off of proof checking. Referees can focus on relevance. Cultural monument to mathematics.
Chip Verification Formal vs. testbench Comparison verification NP-Complete IBM, Intel, AMD successes
Software Verification Hardware is more economically viable More design effort put into software => Software verification is viable Especially useful for critical applications: safety, e-commerce, military
Software Verification Paradox What will verify the verification program? Pragmatism does not demand ideal accuracy Significant improvement enough
More Information Our website: demonstrations of theorem proving tools online additional research
Credits Thank you to Professor David Dill for information and support through e-mail and in person.
Dostları ilə paylaş: |