Progress in the Development of Automated Theorem Proving for Higher-Order Logic
From MaRDI portal
Publication:5191100
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
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
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