Propositional Theorem Proving Methods Overview

 
Propositional Theorem Proving
 
 
Outline
 
III. Forward and backward chaining
 
IV. Effective propositional model checking
 
* Figures are from the 
unless a source is specifically cited.
textbook site
 
II. Horn clauses
 
I. The resolution algorithm
 
 
Resolution Algorithm
 
 
The process ends in one of two situations below:
 
// no new clauses can be added.
Completeness of Resolution
 
II. Horn Clauses
 
Why Horn Clauses?
 
 
 Every definite clause can be written as an implication.
Horn clauses are the basis of logic programming, and play an 
important role in automated theorem proving.
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.
 
(cont’d)
 
 
 Inferences with Horn clauses are through 
forward- and backward-
chaining
   algorithms.
Logic programming
 
(natural inference steps easy for humans to follow)
 
size of the KB
III. Forward Chaining
 
single proposition 
symbol
 Begins from positive literals (facts).
 If all the premises of an implications are known,
   then add its conclusion to KB (as a new fact).
Example of Forward Chaining
 
KB
: 
AND-OR graph representation
Execution
 
 
Soundness
 of forward chaining: every inference is an application of Modus Ponens.
 
Completeness
: every entailed atomic sentences will be derived.
Backward Chaining
 
 
AND-OR graph search!
 
Forward vs. Backward Chaing
 
 
 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.
 
 Applicable range
 
  
Prove the entailment of a single proposition symbol
 
  
KB consists of definite clauses only.
IV. Effective Propositional Model
Checking
 
 
 
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 (W
ALK
SAT algorithm)
 
One sentence in propositional logic (PL)
DPLL Algorithm
 
Davis, Putnam, Logemann, and Loveland (1960, 1962)
 
Recursion Tree
 
 
Dealing with
pure symbols
only
 
Dealing with
unit clauses
only
Example (Exercise 7.25)
 
Convertion into clauses
 
 
Early termination
 
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.
The W
ALK
SAT Algorithm
 
Slide Note
Embed
Share

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.


Uploaded on Sep 28, 2024 | 0 Views


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


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

  2. I. Proving ?1,2 in the Wumpus World ( ?1,1 ?1,2 ?2,1) ( ?1,2 ?1,1) ( ?2,1 ?1,1)

  3. 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 ?.

  4. 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 ? .

  5. 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 ??

  6. 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. ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?

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

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

  9. Example of Forward Chaining KB: AND-OR graph representation Q.KB ??

  10. Execution Soundness of forward chaining: every inference is an application of Modus Ponens. Completeness: every entailed atomic sentences will be derived.

  11. 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!

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

  13. 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)

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

  15. Recursion Tree DPLL Dealing with pure symbols only DPLL Dealing with unit clauses only DPLL DPLL( ,{? = ????}) DPLL( ,{? = ?????})

  16. Example (Exercise 7.25) ?1: ? ? ? ?2: ? ? ?3: ? ? ?1: ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? Convertion into clauses ? ? ? ( ? ?) ? ?4: ? ? ?2: ? ? ?5: ? ? ? ?3: ? ? ? ?6: ? ? ?4: ? ? ?7: ? ? ?5: ? ? ?6: ? ? ?8: ? ?

  17. ? ? ? ? ? ? ?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 ?

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

  19. The WALKSAT Algorithm

More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#