AUTO2, a saturation-based heuristic prover for higher-order logic

DOI10.1007/978-3-319-43144-4_27MaRDI QIDQ2829278zbMATH OpenOpenAlexFDO

Authors Bohua Zhan

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1605.07577

Mathematics Subject Classification ID

Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Abstract: We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core algorithm is a best-first search through the space of propositions derivable from the initial assumptions, where new propositions are added by user-defined functions called proof steps. We implemented the prover in Isabelle/HOL, and applied it to several formalization projects in mathematics and computer science, demonstrating the high level of automation it can provide in a variety of possible proof tasks.

Recommendations

• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Automatic proof and disproof in Isabelle/HOL
• Satallax: An Automatic Higher-Order Prover
• The higher-order prover \textsc{Leo}-II
• Formalizing Bachmair and Ganzinger's ordered resolution prover

Cites work

• A comparison of Mizar and Isar
• A fully automatic theorem prover with human-style output
• A heuristic prover for real inequalities
• Efficient E-Matching for SMT Solvers
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 1543300 (Why is no real title available?)
• Imperative Functional Programming with Isabelle/HOL
• Sledgehammer: judgement day

Cited in

(8)

• A verified proof checker for higher-order logic
• On the use of autarkies for satisfiability decision
• The higher-order prover \textsc{Leo}-II
• Satallax: An Automatic Higher-Order Prover
• AUTO2
• scientific article; zbMATH DE number 1341622 (Why is no real title available?)
• Itauto: An Extensible Intuitionistic SAT Solver
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• PVS
• Isar
• Mizar
• z3
• HOL
• Sledgehammer

This page was built for publication: AUTO2, a saturation-based heuristic prover for higher-order logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829278)