A parallelized theorem prover for a logic with parallel execution

DOI10.1007/978-3-642-39634-2_31MaRDI QIDQ5327362zbMATH OpenOpenAlexFDO

Authors David L. Rager, Warren A. jun. Hunt, Matt Kaufmann

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39634-2_31

zbMATH Keywords

ACL2functional languageparallel execution for a formal logicparallel theorem proving

Mathematics Subject Classification ID

Recommendations

• Pervasive parallelism in highly-trustable interactive theorem proving systems
• Parallelization of a hyper-linking-based theorem prover
• scientific article; zbMATH DE number 4164187
• Shared-memory multiprocessing for interactive theorem proving
• scientific article; zbMATH DE number 4180829

Cited in

(8)

• PARTHENON: A parallel theorem prover for non-horn clauses
• Parallelization of a hyper-linking-based theorem prover
• Pervasive parallelism in highly-trustable interactive theorem proving systems
• scientific article; zbMATH DE number 4180829 (Why is no real title available?)
• scientific article; zbMATH DE number 1086866 (Why is no real title available?)
• Shared-memory multiprocessing for interactive theorem proving
• Parallelizing the \(\text{Mur}\varphi\) verifier
• A cooperative parallelization approach for property-directed \(k\)-induction

Describes a project that uses

Uses Software

• ACL2
• Isabelle
• PVS
• Maude
• PARTHEO
• SicoTHEO

This page was built for publication: A parallelized theorem prover for a logic with parallel execution

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