Zenon

swMATH6753MaRDI QIDQ18828FDOQ18828

Author name not available (Why is that?)

Described by source

• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

Cited In (19)

• 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
• Invariants for the FoCaL language
• Resolution is cut-free
• 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