Zenon
From MaRDI portal
Software:18828
swMATH6753MaRDI QIDQ18828FDOQ18828
Author name not available (Why is that?)
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