Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
From MaRDI portal
Publication:3949989
DOI10.1145/322307.322308zbMath0488.68056OpenAlexW2038464985WikidataQ124796661 ScholiaQ124796661MaRDI QIDQ3949989
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
model generationternary Boolean algebracounterexample generationapplication of theorem proversautomatic search of counterexamples
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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