Propositional Theorem Proving Methods Overview
The overview covers essential techniques in propositional theorem proving including the resolution algorithm, Horn clauses, forward and backward chaining, and effective propositional model checking. It discusses methods such as resolution closure, completeness of resolution, and the significance of Horn clauses in logic programming. The content emphasizes the importance of these methods in automated theorem proving and logic programming due to their computational efficiency and natural inference steps.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Propositional Theorem Proving Outline I. The resolution algorithm II. Horn clauses III. Forward and backward chaining IV. Effective propositional model checking * Figures are from the textbook site unless a source is specifically cited.
I. Proving ?1,2 in the Wumpus World ( ?1,1 ?1,2 ?2,1) ( ?1,2 ?1,1) ( ?2,1 ?1,1)
Resolution Algorithm // no new clauses can be added. The process ends in one of two situations below: No new clauses can be added, in which case KB does not entail ?; Two clauses resolve to yield the empty clause, in which case KB entails ?.
Completeness of Resolution Given a set of clauses S, its resolution closure RC(?) includes all the clauses in ? as well as all the resolvents from repeated applications of the resolution rule. RC(?) is finite because only 3?distinct clauses can be constructed out of ? propositional symbols appearing in S. Ground Resolution Theorem: If ? is unsatisfiable, then RC(?) contains the empty clause . We can construct a proof by explicitly generating an assignment for ? if RC ? .
II. Horn Clauses A clause is called a Horn clause if it contains 1 positive literal. ?: positive literal ?: negative literal Definite clause (1 positive literal and 0 negative literal) ? ? ? ? ? ? rain outside wet rain outside wet ?1 ?2 ?? ? (?1 ?2 ??) ? Fact (1 positive literal and 0 negative literal) true ?1,2 ?1,2 Goal clause (0 positive literal and 1 negative literal) (?1 ?2 ??) false ?1 ?2 ??
Why Horn Clauses? Horn clauses are the basis of logic programming, and play an important role in automated theorem proving. Every definite clause can be written as an implication. ?1 ?2 ?? ? (?1 ?2 ??) ? ? (?1 ?2 ??) Q :- P1, P2, , Pk. (Prolog programming language) Horn clauses are closed under resolution, i.e., the resolvent of two Horn clauses is still a Horn clause. ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?
(contd) Inferences with Horn clauses are through forward- and backward-chaining algorithms. Logic programming (natural inference steps easy for humans to follow) Low computational complexity: deciding entailment with Horn clauses takes ? ? time. size of the KB
III. Forward Chaining Begins from positive literals (facts). QuestionKB ?? If all the premises of an implications are known, then add its conclusion to KB (as a new fact). single proposition symbol Continues until ? is added or no further inferences can be made.
Example of Forward Chaining KB: AND-OR graph representation Q.KB ??
Execution Soundness of forward chaining: every inference is an application of Modus Ponens. Completeness: every entailed atomic sentences will be derived.
Backward Chaining If ? is true, no work is needed. Otherwise, finds implications in the KB whose conclusion is ?. If all the premises of one of these implications can be proved true (recursively by backward chaining), then ? is true. Q.KB ?? AND-OR graph search!
Forward vs. Backward Chaing Applicable range Prove the entailment of a single proposition symbol KB consists of definite clauses only. Either ? or ?1 ?2 ?? ? Forward chaining is data-driven, automatic, unconscious processing. It may perform a lot of work that is irrelevant to the goal. Backward chaining is goal-driven, and appropriate for problem solving. It may run in time sublinear in the size of KB, since it touches only relevant facts.
IV. Effective Propositional Model Checking KB ? if and only if KB ? is unsatisfiable. One sentence in propositional logic (PL) Satisfiability problem Is a sentence ? in PL satisfiable? Cast the problem as one of constraint satisfaction. Many combinatorial problems in computer science can be reduced to checking the satisfiability of a propositional sentence. Complete backtracking search (DPLL algorithm) Incomplete local search (WALKSAT algorithm)
DPLL Algorithm Davis, Putnam, Logemann, and Loveland (1960, 1962) With enhancements, modern solvers can handle a problem with a multiple of 107 variables. Early termination: a clause is true if any of its literals is true. E.g., ? ? ? is true if ? is true (regardless of the values assigned to ? and ?). Pure symbol: a symbol appearing always positive or always negative in all clauses. E.g., ? and ? are pure in ? ?, ? ?, ? ? while ? is not pure. Assignment ? true will reduce the set to ? ?, enabling ? to become a pure symbol. Truth value to assign to ? Unit clause propagation on a clause in which all literals but one are assigned false. E.g., ? ? simplifies to the unit clause ? if ? =true.
Recursion Tree DPLL Dealing with pure symbols only DPLL Dealing with unit clauses only DPLL DPLL( ,{? = ????}) DPLL( ,{? = ?????})
Example (Exercise 7.25) ?1: ? ? ? ?2: ? ? ?3: ? ? ?1: ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? Convertion into clauses ? ? ? ( ? ?) ? ?4: ? ? ?2: ? ? ?5: ? ? ? ?3: ? ? ? ?6: ? ? ?4: ? ? ?7: ? ? ?5: ? ? ?6: ? ? ?8: ? ?
? ? ? ? ? ? ?1: ? ? ? ?3: ? ? ?5: ? ? ? ?2: ? ? ?4: ? ? ?1 -- ?8 ?6: ? ? ?8: ? ? Pure symbol ?7: ? ? ?1 -- ?3 ?5 -- ?8 ? ?2 ?16: ? ?3 ?17: ? ?5 -- ?8 ? ?1 ?9: ? ? ? ? ? ?5 -- ?8 Unit clause propagation ?6 ?18: ? ?17: ? ?5 ?10: ? ? ?7 ?11:? ?8 ?12:? ?6 ?14: ? ? ? ? ? ? ? ?9 ?15: ? ? ? ? Unit clause propagation Pure symbol Unit clause propagation ?10 ?13: ? ?12:? ? ? ? ? ?15 ? ? ? ? ? ? ? ? ? Early termination Unit clause propagation ? ? ?13 ? ? ? Early termination ?
Local Search Algorithms Take steps in the space of complete assignments, flipping the truth value of one symbol at a time. Use an evaluation that counts the number of unsatisfied clauses. Escape local minima using various forms of randomness. Find a good balance between greediness and randomness.
