Zenon
From MaRDI portal
Cited in
(35)- Integrating simplex with tableaux
- Implicit definitions with differential equations for KeYmaera X (system description)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Termination Proofs for Recursive Functions in FoCaLiZe
- EUCLID
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Automated constructivization of proofs
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Automated proof of Bell-LaPadula security properties
- Functional Testing in the Focal Environment
- I-SATCHMO
- Atelier B
- FoCaL
- OpenAxiom
- BWare
- FoCaLiZe
- Beagle
- dedukti
- CoqMT
- SNARK
- HARP
- Focalide
- CoqInE
- ArchSAT
- ekstrakto
- Resolution is cut-free
- Invariants for the FoCaL language
- Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
- Theorem proving as constraint solving with coherent logic
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover
- Soundly proving B method formulæ using typed sequent calculus
- ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
- scientific article; zbMATH DE number 7178363 (Why is no real title available?)
- Verifying B proof rules using deep embedding and automated theorem proving
This page was built for software: Zenon
