Publication:4809048
From MaRDI portal
zbMath1072.68578MaRDI QIDQ4809048
Publication date: 12 August 2004
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2392/23920134.htm
03B35: Mechanization of proofs and logical operations
Related Items
Unnamed Item, Using First-Order Theorem Provers in the Jahob Data Structure Verification System, Mark Stickel: his earliest work, The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4, Combined reasoning by automated cooperation, Integrating external deduction tools with ACL2, Efficiently checking propositional refutations in HOL theorem provers, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\), Translating higher-order clauses to first-order clauses, Validating QBF Validity in HOL4, Proving Valid Quantified Boolean Formulas in HOL Light, Expressing Polymorphic Types in a Many-Sorted Language
Uses Software