Catalogue of Artificial Intelligence Techniques
Aliases: Use of Models
Keywords: Horn clauses
Categories: Theorem Proving
Author(s): Alan Bundy
A technique for pruning a Search Space of a logical inference mechanism, e.g., Resolution or Natural Deduction. One or more models are given of the axioms and hypotheses of a problem. If a model is not a counterexample then the goal is also true in that model. All subgoals false in any model are pruned from the search space. This technique preserves completeness if the problem consists only of Horn clauses.
- Bundy, A., The Computer Modelling of Mathematical Reasoning, Academic Press, London, 1983, pp.169--189, also second edition, 1986