Pages that link to "Item:Q1595929"
From MaRDI portal
The following pages link to Structured theory development for a mechanized logic (Q1595929):
Displaying 19 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- On definitions of constants and types in HOL (Q287358) (← links)
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks (Q437040) (← links)
- Proof pearl: a formal proof of Higman's lemma in ACL2 (Q438550) (← links)
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 (Q540690) (← links)
- Rewriting with equivalence relations in ACL2 (Q928668) (← links)
- Integrating external deduction tools with ACL2 (Q1006728) (← links)
- A verified common lisp implementation of Buchberger's algorithm in ACL2 (Q1034553) (← links)
- Formal logics of discovery and hypothesis formation by machine (Q1870530) (← links)
- Modelling algebraic structures and morphisms in ACL2 (Q2349534) (← links)
- Formal verification of a generic framework to synthesize SAT-provers (Q2583288) (← links)
- Theory extension in ACL2(r) (Q2642461) (← links)
- Towards a mechanically checked theory of computation. The ACL2 project (Q2734953) (← links)
- ACL2s: ``the ACL2 sedan'' (Q2867932) (← links)
- Towards Robustness Analysis Using PVS (Q3087998) (← links)
- An ACL2 Tutorial (Q3543644) (← links)
- A theorem prover for a computational logic (Q6488518) (← links)
- Formal verification of a deadlock detection algorithm (Q6586533) (← links)
- A step-indexing approach to partial functions (Q6587252) (← links)
