Automation for interactive proof: first prototype

DOI10.1016/J.IC.2005.05.010MaRDI QIDQ2432769zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

interactive theorem provers

Mathematics Subject Classification ID

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

• scientific article; zbMATH DE number 1614717 (Why is no real title available?)
• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 1543300 (Why is no real title available?)
• scientific article; zbMATH DE number 1552511 (Why is no real title available?)
• scientific article; zbMATH DE number 1765682 (Why is no real title available?)
• scientific article; zbMATH DE number 2154400 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A unification algorithm for typed -calculus
• Automated Reasoning
• Automated proof construction in type theory using resolution
• Combining superposition, sorts and splitting
• Computing small clause normal forms
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Handbook of automated reasoning. In 2 vols
• Isabelle/HOL. A proof assistant for higher-order logic
• The TPTP problem library. CNF release v1. 2. 1
• The foundation of a generic theorem prover

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
• scientific article; zbMATH DE number 2090293 (Why is no real title available?)
• Iterative dialogues and automated proof.
• From informal to formal proofs in Euclidean geometry
• Combined reasoning by automated cooperation
• scientific article; zbMATH DE number 1552511 (Why is no real title available?)
• 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
• TPS: A hybrid automatic-interactive system for developing proofs
• From LCF to Isabelle/HOL
• Translating higher-order clauses to first-order clauses
• Automated Reasoning
• 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

Describes a project that uses

Uses Software

• TRAMP
• Gandalf
• HOL
• Proof General
• Isar
• Metis
• TPTP
• PVS
• VAMPIRE
• Isabelle/Isar
• Isabelle/HOL
• ML
• Isabelle

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)