Catalogue of Artificial Intelligence Techniques

   

Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

Paramodulation

Keywords: clause, rule of inference, unifier

Categories: Theorem Proving


Author(s): Alan Bundy

A rule of inference of Predicate Calculus, used to deduce a new formula from two old ones. It is used in Automatic Theorem Proving, in conjunction with Resolution, as an alternative to the axioms of equality. All the three formulae involved must be in Clausal Form. If C[ ] and D are clauses, where C[ ] indicates that C contains a particular occurrence of , then the rule is:

C[t']         D s=t (C[s] D)          C[t']         Dt=s (C[s] D)

where is the most general unifier of and , and is obtained by Unification. C[ ] indicates that only the particular occurrence of is replaced by in C, other occurrences of are untouched.


References:


Comments:

Add Comment

No comments.