How to avoid the formal verification of a theorem prover

DOI10.1093/JIGPAL/9.1.1MaRDI QIDQ2708306zbMATH OpenOpenAlexFDO

Authors Alessandro Avellone, Marco Benini, Ugo Moscato

Publication date 17 April 2001

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/11cf51412aaa6745fb7869e37c22fd308f841e33

zbMATH Keywords

tableau-based theorem provertheorem prover

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Testing a saturation-based theorem prover: experiences and challenges
• scientific article; zbMATH DE number 3880145
• The Proof Certifier Checkers
• scientific article; zbMATH DE number 1746646
• Foundational proof certificates in first-order logic

This page was built for publication: How to avoid the formal verification of a theorem prover

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2708306)