Automation for interactive proof: first prototype
From MaRDI portal
Publication:2432769
DOI10.1016/j.ic.2005.05.010zbMath1103.68113OpenAlexW2017989625WikidataQ57382638 ScholiaQ57382638MaRDI QIDQ2432769
Claire Quigley, Jia Meng, Lawrence Charles Paulson
Publication date: 25 October 2006
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2005.05.010
Related Items
From informal to formal proofs in Euclidean geometry, The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0, Automated flaw detection in algebraic specifications, Automating Algebraic Specifications of Non-freely Generated Data Types, Combined reasoning by automated cooperation, Translating higher-order clauses to first-order clauses, An Interactive Driver for Goal-directed Proof Strategies, Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Proverʼs Palette, From LCF to Isabelle/HOL, The Matita Interactive Theorem Prover, Bounded Relational Analysis of Free Data Types, Lightweight relevance filtering for machine-generated resolution problems, Composable Discovery Engines for Interactive Theorem Proving, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Combining Isabelle and QEPCAD-B in the Prover’s Palette
Uses Software
Cites Work
- A unification algorithm for typed \(\overline\lambda\)-calculus
- The TPTP problem library. CNF release v1. 2. 1
- Isabelle/HOL. A proof assistant for higher-order logic
- The foundation of a generic theorem prover
- Automated proof construction in type theory using resolution
- Automated Reasoning
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
