swMATH6753MaRDI QIDQ18828FDOQ18828
Author name not available (Why is that?)
Official website: http://deducteam.gforge.inria.fr/zenonmodulo/
Cited In (35)
- Implicit definitions with differential equations for KeYmaera X (system description)
- Termination Proofs for Recursive Functions in FoCaLiZe
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- 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
- Functional Testing in the Focal Environment
- Automated proof of Bell-LaPadula security properties
- I-SATCHMO
- Atelier B
- Invariants for the FoCaL language
- Resolution is cut-free
- FoCaL
- OpenAxiom
- BWare
- FoCaLiZe
- Beagle
- dedukti
- CoqMT
- SNARK
- HARP
- Focalide
- CoqInE
- ArchSAT
- ekstrakto
- EUCLID
- 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
- Title not available (Why is that?)
- ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti
- Verifying B proof rules using deep embedding and automated theorem proving
- Integrating simplex with tableaux
This page was built for software: Zenon
