Satallax
From MaRDI portal
Software:18920
swMATH6849MaRDI QIDQ18920FDOQ18920
Author name not available (Why is that?)
Cited In (62)
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Restricted combinatory unification
- Extending Sledgehammer with SMT solvers
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- A realizability interpretation of Church's simple theory of types
- Superposition with lambdas
- Lash 1.0 (system description)
- Improving automation for higher-order proof steps
- Embedding and automating conditional logics in classical higher-order logic
- The CADE-26 automated theorem proving system competition -- CASC-26
- Scavenger 0.1: a theorem prover based on conflict resolution
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- HOL Based First-Order Modal Logic Provers
- Cut-elimination for quantified conditional logic
- Extensional higher-order paramodulation in Leo-III
- Title not available (Why is that?)
- Functions-as-constructors higher-order unification: extended pattern unification
- Title not available (Why is that?)
- 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
- Deep network guided proof search
- Analytic tableaux for higher-order logic with choice
- Reducing higher-order theorem proving to a sequence of SAT problems
- Making higher-order superposition work
- Superposition with lambdas
- A combinator-based superposition calculus for higher-order logic
- Combining and automating classical and non-classical logics in classical higher-order logics
- Internal guidance for Satallax
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Effective normalization techniques for HOL
- Title not available (Why is that?)
- Reducing higher-order theorem proving to a sequence of SAT problems
- Monte Carlo tableau proof search
- GRUNGE: a grand unified ATP challenge
- Theorem proving in large formal mathematics as an emerging AI field
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- Limited second-order functionality in a first-order setting
- Superposition for \(\lambda\)-free higher-order logic
- 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
- Extending SMT solvers to higher-order logic
- 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
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- Agent-based HOL reasoning
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- LEO-II and Satallax on the Sledgehammer test bench
- The higher-order prover Leo-III
- Hammering towards QED
- On logic embeddings and Gödel's God
- Functions-as-constructors Higher-order Unification
- Theorem provers for every normal modal logic
- TacticToe: learning to reason with HOL4 tactics
- A Knuth-Bendix-like ordering for orienting combinator equations
- Interacting with Modal Logics in the Coq Proof Assistant
- Making higher-order superposition work
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Title not available (Why is that?)
This page was built for software: Satallax
