Satallax: An Automatic Higher-Order Prover
From MaRDI portal
Publication:2908482
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
(48)- Restricted combinatory unification
- Lash 1.0 (system description)
- Improving automation for higher-order proof steps
- A realizability interpretation of Church's simple theory of types
- Superposition with lambdas
- Solving modal logic problems by translation to higher-order logic
- The CADE-26 automated theorem proving system competition -- CASC-26
- AVATAR: The Architecture for First-Order Theorem Provers
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Cut-elimination for quantified conditional logic
- Extensional higher-order paramodulation in Leo-III
- Functions-as-constructors higher-order unification: extended pattern unification
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- The MET: The Art of Flexible Reasoning with Modalities
- 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
- Proofs and reconstructions
- Reducing higher-order theorem proving to a sequence of SAT problems
- A combinator-based superposition calculus for higher-order logic
- Internal guidance for Satallax
- Superposition with lambdas
- Effective normalization techniques for HOL
- Superposition for higher-order logic
- Reducing higher-order theorem proving to a sequence of SAT problems
- scientific article; zbMATH DE number 7471678 (Why is no real title available?)
- Satallax
- GRUNGE: a grand unified ATP challenge
- scientific article; zbMATH DE number 4094866 (Why is no real title available?)
- Theorem proving in large formal mathematics as an emerging AI field
- Higher-order modal logics: automation and applications
- Superposition for full higher-order logic
- Limited second-order functionality in a first-order setting
- 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
- Extending SMT solvers to higher-order logic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Itauto: An Extensible Intuitionistic SAT Solver
- 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
- Extending a high-performance prover to higher-order logic
- Agent-based HOL reasoning
- AUTO2, a saturation-based heuristic prover for higher-order logic
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- A Knuth-Bendix-like ordering for orienting combinator equations
- Interacting with Modal Logics in the Coq Proof Assistant
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)
