Automation for interactive proof: first prototype

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

zbMATH Keywords

interactive theorem provers

Mathematics Subject Classification ID

Related Items (15)

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

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• PVS
• TPTP
• Metis_
• Isar
• Proof General
• HOL
• Gandalf
• TRAMP

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

This page was built for publication: Automation for interactive proof: first prototype