Structured theory development for a mechanized logic
From MaRDI portal
Publication:1595929
DOI10.1023/A:1026517200045zbMath0971.03017OpenAlexW1588366745MaRDI QIDQ1595929
J. Strother Moore, Matt Kaufmann
Publication date: 18 February 2001
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1026517200045
Related Items (13)
The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ On definitions of constants and types in HOL ⋮ Theory extension in ACL2(r) ⋮ Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks ⋮ Proof pearl: a formal proof of Higman's lemma in ACL2 ⋮ Rewriting with equivalence relations in ACL2 ⋮ An ACL2 Tutorial ⋮ The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 ⋮ Integrating external deduction tools with ACL2 ⋮ Towards Robustness Analysis Using PVS ⋮ A verified common lisp implementation of Buchberger's algorithm in ACL2 ⋮ Formal verification of a generic framework to synthesize SAT-provers ⋮ Modelling algebraic structures and morphisms in ACL2
Uses Software
This page was built for publication: Structured theory development for a mechanized logic
