Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML


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[t ] and D are clauses, where C[t ] indicates that C contains a particular occurrence of t , 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 t and t , and is obtained by Unification. C[s ] indicates that only the particular occurrence of t is replaced by s in C, other occurrences of t are untouched.



Add Comment

No comments.