# Catalogue of Artificial Intelligence Techniques

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.

### References:

- Bundy, A.,
*The Computer Modelling of Mathematical Reasoning*, Academic Press, London, 1983, pp.169--189, also second edition, 1986 .

### Comments:

No comments.