Progress in the Development of Automated Theorem Proving for Higher-Order Logic

DOI10.1007/978-3-642-02959-2_8zbMath1250.68236OpenAlexW1531639736MaRDI QIDQ5191100

Christoph Benzmüller, Frank Theiß, Geoff Sutcliffe, Chad Edward Brown

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_8

Mathematics Subject Classification ID

Related Items

Unnamed Item, Analytic tableaux for higher-order logic with choice, Analytic Tableaux for Higher-Order Logic with Choice, Superposition with lambdas, Superposition with lambdas

Uses Software

• ILTP
• LEO-II
• TPS
• Isabelle/HOL
• VAMPIRE
• THF0
• SPASS
• TPTP
• Metis_
• Proof General
• Twelf
• Automath
• OMDoc
• E Theorem Prover
• Leo
• IDV

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The seventeen provers of the world. Foreword by Dana S. Scott..
• TPS: A hybrid automatic-interactive system for developing proofs
• Computer supported mathematics with \(\Omega\)MEGA
• The ILTP problem library for intuitionistic logic
• On connections and higher-order logic
• Combined reasoning by automated cooperation
• A compact representation of proofs
• A unification algorithm for typed \(\bar\lambda\)-calculus
• The TPTP problem library. CNF release v1. 2. 1
• Isabelle/HOL. A proof assistant for higher-order logic
• An Interactive Derivation Viewer
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• System Description: Spass Version 3.0
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
• Theorem Proving via General Matings
• On Matrices with Connections
• Higher-order semantics and extensionality
• Theorem Proving in Higher Order Logics
• Resolution in type theory