---
title: "Completeness Theorems for Semantic Resolution in Consequence-Finding"
authors:
  - "James R. Slagle"
  - "Chin-Liang Chang"
  - "Richard C. T. Lee"
doi: ""
url: "https://ijcai.org/proceedings/1969/27"
pdf: "https://ijcai.org/proceedings/1969/0027.pdf"
venue: "Proceedings of the First International Joint Conference on Artificial Intelligence"
year: 1969
pages: "281-286"
track: "Theorem Proving"
keywords:
---

# Completeness Theorems for Semantic Resolution in Consequence-Finding

James R. Slagle, Chin-Liang Chang, Richard C. T. Lee

*Proceedings of the First International Joint Conference on Artificial Intelligence*, pages 281-286.

## Abstract

The object of consequence-finding is to deduce logical consequences from a set of axioms. The theory of J.R. Slagle's semantic resolution principle, an inference rule for first-order predicate calculus, is extended to consequence-finding. Given an interpretation I, it is proved that any prime (non-trivial) consequence, which is false in I, can be derived from a set of axioms by applying !-(semantic) resolution.