Satallax: An Automatic Higher-Order Prover
From MaRDI portal
Publication:2908482
DOI10.1007/978-3-642-31365-3_11zbMATH Open1358.68250OpenAlexW79561349MaRDI QIDQ2908482FDOQ2908482
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
Recommendations
- AUTO2, a saturation-based heuristic prover for higher-order logic
- A comprehensive framework for saturation theorem proving
- A comprehensive framework for saturation theorem proving
- Satisfiability calculus: an abstract formulation of semantic proof systems
- Formal verification of a generic framework to synthesize SAT-provers
- scientific article
- Verification in ACL2 of a generic framework to synthesize SAT-provers
- Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
- SAT-based proof search in intermediate propositional logics
Cited In (45)
- Restricted combinatory unification
- A realizability interpretation of Church's simple theory of types
- Solving modal logic problems by translation to higher-order logic
- Superposition with lambdas
- Lash 1.0 (system description)
- Improving automation for higher-order proof steps
- Agent-Based HOL Reasoning
- AVATAR: The Architecture for First-Order Theorem Provers
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Cut-elimination for quantified conditional logic
- Extensional higher-order paramodulation in Leo-III
- The MET: The Art of Flexible Reasoning with Modalities
- Title not available (Why is that?)
- Functions-as-constructors higher-order unification: extended pattern unification
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
- 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
- Superposition with lambdas
- A combinator-based superposition calculus for higher-order logic
- Superposition for higher-order logic
- Title not available (Why is that?)
- GRUNGE: a grand unified ATP challenge
- Title not available (Why is that?)
- Satallax
- Proofs and Reconstructions
- Internal Guidance for Satallax
- Superposition for full higher-order logic
- Limited second-order functionality in a first-order setting
- Effective Normalization Techniques for HOL
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- The CADE-26 automated theorem proving system competition – CASC-26
- Extending SMT solvers to higher-order logic
- Itauto: An Extensible Intuitionistic SAT Solver
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Practical Proof Search for Coq by Type Inhabitation
- Automating free logic in HOL, with an experimental application in category theory
- The 11th IJCAR automated theorem proving system competition – CASC-J11
- Higher-Order Modal Logics: Automation and Applications
- Extending a high-performance prover to higher-order logic
- A Knuth-Bendix-like ordering for orienting combinator equations
- Interacting with Modal Logics in the Coq Proof Assistant
Uses Software
This page was built for publication: Satallax: An Automatic Higher-Order Prover
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2908482)
