Introduction Mechanical theorem proving is an important subject in artificial intelligence



Yüklə 519 b.
tarix29.10.2017
ölçüsü519 b.
#7260


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

  • Philosophical issues regarding a mechanical theorem prover

  • 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

  • Truth Table



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



Herbrand’s theorem… and a little history

  • 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,

  • ulp+ = smallest representable increment



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



The QED Project- Hoped Benefits

  • 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.



Yüklə 519 b.

Dostları ilə paylaş:




Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©genderi.org 2024
rəhbərliyinə müraciət

    Ana səhifə