Satallax: An Automatic Higher-Order Prover
From MaRDI portal
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; zbMATH DE number 4094866
- 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
(56)- Satallax
- Superposition for full higher-order logic
- A Knuth-Bendix-like ordering for orienting combinator equations
- A combinator-based superposition calculus for higher-order logic
- Lash 1.0 (system description)
- Functions-as-constructors higher-order unification: extended pattern unification
- Automating free logic in HOL, with an experimental application in category theory
- Limited second-order functionality in a first-order setting
- Extending SMT solvers to higher-order logic
- Restricted combinatory unification
- GRUNGE: a grand unified ATP challenge
- Reducing higher-order theorem proving to a sequence of SAT problems
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Cut-elimination for quantified conditional logic
- Extensional higher-order paramodulation in Leo-III
- Internal guidance for Satallax
- Effective normalization techniques for HOL
- Agent-based HOL reasoning
- AUTO2, a saturation-based heuristic prover for higher-order 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
- AVATAR: The Architecture for First-Order Theorem Provers
- Proofs and reconstructions
- Higher-order modal logics: automation and applications
- Interacting with Modal Logics in the Coq Proof Assistant
- \textsc{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
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- scientific article; zbMATH DE number 1301855 (Why is no real title available?)
- A realizability interpretation of Church's simple theory of types
- Theorem proving in large formal mathematics as an emerging AI field
- Superposition for lambda-free higher-order logic
- Efficient full higher-order unification
- Practical Proof Search for Coq by Type Inhabitation
- The CADE-28 Automated Theorem Proving System Competition – CASC-28
- The CADE-26 automated theorem proving system competition -- CASC-26
- Reducing higher-order theorem proving to a sequence of SAT problems
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Superposition with lambdas
- Superposition with lambdas
- 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
- Itauto: An Extensible Intuitionistic SAT Solver
- Extending a high-performance prover to higher-order logic
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- The dependently typed higher-order form for the TPTP world
- Efficient full higher-order unification
- Dependently typed higher-order logic
- Notes on Gödel's and Scott's variants of the ontological argument
- Experiments with choice in dependently-typed higher-order logic
- Tableaux for automated reasoning in dependently-typed higher-order logic
- An empirical assessment of progress in automated theorem proving
- Improving automation for higher-order proof steps
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)
