Bry, François and Manthey, Rainer
Proving Finite Satisfiability of Deductive Databases.
1st Workshop on Computer Science Logic (CSL), 12.10.-16.10.1987, Karlsruhe.
It is shown how certain refutation methods can be extended into semi-decision
procedures that are complete for both unsatisfiability and finite satisfiability. The proposed extension
is justified by a new characterization of finite satisfiability. This research was motivated
by a database design problem: Deduction rules and integrity constraints in definite databases
have to be finitely satisfiable