Solving open questions and other challenge problems using proof sketches
From MaRDI portal
Publication:5951528
DOI10.1023/A:1010639725972zbMath1006.03511OpenAlexW1510627098MaRDI QIDQ5951528
Publication date: 7 January 2002
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1010639725972
automated theorem provingcondensed detachmentlinked UR-resolutionproof sketchsearching for proofs in logical systems
Related Items
Axiomatizing the skew Boolean propositional calculus, Constructive logic with strong negation is a substructural logic. I, A Geometric Procedure with Prover9, Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction, Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach, MOUFANG MAGMAS WITH INVERSES, Proof simplification and automated theorem proving, Constructive logic with strong negation is a substructural logic. II, Compatibly involutive residuated lattices and the Nelson identity, A FORMAL SYSTEM FOR EUCLID’SELEMENTS, A Wos Challenge Met, A posthumous contribution by Larry Wos: excerpts from an unpublished column
Uses Software
