A Hyperresolution-based Proof Procedure and Its Implementation in Prolog
Generate an AI Snapshot to get a quick, structured summary of this paper.
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The procedure described in this paper is the basis of a program called SATCHMO (SATisfiability CHecking by MOdel generation) that has been implemented at ECRC as part of a prototype schema design system for logic databases.
Abstract
Our work on automated deduction has been motivated by database problems. The set of deduction rules and integrity constraints of a logic database can be considered as axioms of a first-order theory while the actual sets of facts constitute (finite) models of this theory. Satisfiability of the underlying axioms is a necessary prerequisite for any logic database. The procedure described in this paper is the basis of a program called SATCHMO (SATisfiability CHecking by MOdel generation) that has been implemented at ECRC as part of a prototype schema design system for logic databases.