Automation for interactive proof: first prototype
From MaRDI portal
Publication:2432769
DOI10.1016/J.IC.2005.05.010zbMATH Open1103.68113OpenAlexW2017989625WikidataQ57382638 ScholiaQ57382638MaRDI QIDQ2432769FDOQ2432769
Authors: Jia Meng, Claire Quigley, Lawrence C. 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
Recommendations
- scientific article; zbMATH DE number 1552511
- Automated constructivization of proofs
- Revitalized automatic proofs: demonstrations
- scientific article; zbMATH DE number 4106274
- A Framework for Interactive Proof
- A light-weight integration of automated and interactive theorem proving
- Publication:3034850
- Interactive Coding for Interactive Proofs
Cites Work
- The TPTP problem library. CNF release v1. 2. 1
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Combining superposition, sorts and splitting
- Title not available (Why is that?)
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Computing small clause normal forms
- Title not available (Why is that?)
- Handbook of automated reasoning. In 2 vols
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Title not available (Why is that?)
- The foundation of a generic theorem prover
- Title not available (Why is that?)
- Title not available (Why is that?)
- Automated Reasoning
- Automated proof construction in type theory using resolution
Cited In (22)
- Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover's palette
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Automating Algebraic Specifications of Non-freely Generated Data Types
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Title not available (Why is that?)
- Iterative dialogues and automated proof.
- From informal to formal proofs in Euclidean geometry
- Title not available (Why is that?)
- Combined reasoning by automated cooperation
- Lightweight relevance filtering for machine-generated resolution problems
- Bounded Relational Analysis of Free Data Types
- Automated flaw detection in algebraic specifications
- Combining Isabelle and QEPCAD-B in the Prover’s Palette
- From LCF to Isabelle/HOL
- TPS: A hybrid automatic-interactive system for developing proofs
- Automated Reasoning
- Translating higher-order clauses to first-order clauses
- How to make ad hoc proof automation less ad hoc
- The Matita interactive theorem prover
- Composable discovery engines for interactive theorem proving
- An Interactive Driver for Goal-directed Proof Strategies
- Source-Level Proof Reconstruction for Interactive Theorem Proving
Uses Software
This page was built for publication: Automation for interactive proof: first prototype
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2432769)
