Satallax: An Automatic Higher-Order Prover
From MaRDI portal
Publication:2908482
DOI10.1007/978-3-642-31365-3_11zbMath1358.68250OpenAlexW79561349MaRDI QIDQ2908482
Publication date: 5 September 2012
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-31365-3_11
Related Items
Cut-elimination for quantified conditional logic ⋮ MaLeS: a framework for automatic tuning of automated theorem provers ⋮ The higher-order prover \textsc{Leo}-II ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ Improving automation for higher-order proof steps ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Interacting with Modal Logics in the Coq Proof Assistant ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Unnamed Item ⋮ A realizability interpretation of Church's simple theory of types ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ The MET: The Art of Flexible Reasoning with Modalities ⋮ Solving modal logic problems by translation to higher-order logic ⋮ Superposition for higher-order logic ⋮ Proofs and Reconstructions ⋮ Higher-Order Modal Logics: Automation and Applications ⋮ Unnamed Item ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Computer-assisted analysis of the Anderson-Hájek ontological controversy ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ Limited second-order functionality in a first-order setting ⋮ Internal Guidance for Satallax ⋮ Effective Normalization Techniques for HOL ⋮ Agent-Based HOL Reasoning ⋮ Superposition for full higher-order logic ⋮ Extending SMT solvers to higher-order logic ⋮ Restricted combinatory unification ⋮ GRUNGE: a grand unified ATP challenge ⋮ Satallax ⋮ A Knuth-Bendix-like ordering for orienting combinator equations ⋮ A combinator-based superposition calculus for higher-order logic ⋮ Lash 1.0 (system description) ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
