AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic

DOI10.1007/978-3-319-43144-4_27zbMath1478.68439arXiv1605.07577OpenAlexW3105824395MaRDI QIDQ2829278

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) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Formalization of the fundamental group in untyped set theory using auto2 ⋮ AUTO2

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• A comparison of Mizar and Isar
• A fully automatic theorem prover with human-style output
• A Heuristic Prover for Real Inequalities
• Imperative Functional Programming with Isabelle/HOL
• Efficient E-Matching for SMT Solvers
• Sledgehammer: Judgement Day

This page was built for publication: AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic