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
• Tableaux Modulo Theories Using Superdeduction
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• Soundly Proving B Method Formulæ Using Typed Sequent Calculus
• 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
• 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
• Automated Constructivization of Proofs
• 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
• Title not available (Why is that?)

This page was built for software: Zenon