Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions

Abstract

Two open questions m ternary Boolean algebras have been answered with the aid of an existmg automated theorem-proving program without recourse to any additional programming. The new automated theorem-provmg techraques developed in answering the open questions are presented here. Essentially, the ex~stmg theorem prover is used m a nonstandard way to seek and verify small fmite models and counterexamples for a first-order axiom system Exhibiting a model of an axiom system proves it consment; this facility complements traditional theorem-provmg methods, which can only prove mconslstency.