Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
From MaRDI portal
Recommendations
Cited in
(20)- Efficiently checking propositional refutations in HOL theorem provers
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Extending Sledgehammer with SMT solvers
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
- Cooperation in heterogeneous theorem prover networks (Diss., Univ. Kaiserslautern)
- versat: A Verified Modern SAT Solver
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Modular SMT proofs for fast reflexive checking inside Coq
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- HOL Light: An Overview
- Linear Arithmetic with Stars
- Combining theories with shared set operations
- scientific article; zbMATH DE number 1222430 (Why is no real title available?)
- scientific article; zbMATH DE number 1285157 (Why is no real title available?)
- Extending Sledgehammer with SMT solvers
- Computer Aided Verification
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Rocket-Fast Proof Checking for SMT Solvers
- Scalable fine-grained proofs for formula processing
- Interoperability of proof systems with SC-TPTP
This page was built for publication: Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2848688)
