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

DOI10.1145/322307.322308zbMath0488.68056OpenAlexW2038464985WikidataQ124796661 ScholiaQ124796661MaRDI QIDQ3949989

Steve Winker

Publication date: 1982

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://www.osti.gov/biblio/6416263

zbMATH Keywords

model generationternary Boolean algebracounterexample generationapplication of theorem proversautomatic search of counterexamples

Mathematics Subject Classification ID

Related Items (12)

The application of automated reasoning to questions in mathematics and logic ⋮ Increasing the efficiency of automated theorem proving ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Simplifying and generalizing formulae in tableaux. Pruning the search space and building models ⋮ A method for simultaneous search for refutations and models by equational constraint solving ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ A method for building models automatically. Experiments with an extension of OTTER ⋮ Semantically guided first-order theorem proving using hyper-linking ⋮ Problems on the generation of finite models ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains ⋮ The problem of guaranteeing the existence of a complete set of reductions

This page was built for publication: Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions