Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
S. Winker · Journal of the ACM · 1982
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.