Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

Semantic Checking

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.



Add Comment

No comments.