An automatic theorem prover for substitution and detachment systems
From MaRDI portal
Publication:1242700
DOI10.1305/ndjfl/1093888213zbMath0368.68086OpenAlexW2011948182MaRDI QIDQ1242700
Publication date: 1978
Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1305/ndjfl/1093888213
Classical propositional logic (03B05) Algorithms in computer science (68W99) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)
Related Items
A finitely axiomatized formalization of predicate calculus with equality, A (machine-oriented) logic based on pattern matching, Meeting the challenge of fifty years of logic, A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains, CODE: A powerful prover for problems of condensed detachment, Condensed detachment as a rule of inference
