The following pages link to Satallax (Q18920):
Displayed 50 items.
- MaLeS: a framework for automatic tuning of automated theorem provers (Q286787) (← links)
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Computer-assisted analysis of the Anderson-Hájek ontological controversy (Q523303) (← links)
- Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- Improving automation for higher-order proof steps (Q831930) (← links)
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas (Q1735326) (← links)
- Superposition for \(\lambda\)-free higher-order logic (Q1799065) (← links)
- The higher-order prover Leo-III (Q1799072) (← links)
- Embedding and automating conditional logics in classical higher-order logic (Q1935597) (← links)
- LEO-II and Satallax on the Sledgehammer test bench (Q1948289) (← links)
- A Knuth-Bendix-like ordering for orienting combinator equations (Q2096451) (← links)
- A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
- Lash 1.0 (system description) (Q2104521) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- Automating free logic in HOL, with an experimental application in category theory (Q2303232) (← links)
- Limited second-order functionality in a first-order setting (Q2303245) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Restricted combinatory unification (Q2305407) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) (Q2305414) (← links)
- Reducing higher-order theorem proving to a sequence of SAT problems (Q2351156) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Cut-elimination for quantified conditional logic (Q2363418) (← links)
- Scavenger 0.1: a theorem prover based on conflict resolution (Q2405260) (← links)
- Monte Carlo tableau proof search (Q2405274) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- On Logic Embeddings and Gödel’s God (Q2787333) (← links)
- Extracting Higher-Order Goals from the Mizar Mathematical Library (Q2817297) (← links)
- Internal Guidance for Satallax (Q2817934) (← links)
- Effective Normalization Techniques for HOL (Q2817937) (← links)
- Agent-Based HOL Reasoning (Q2819202) (← links)
- HOL Based First-Order Modal Logic Provers (Q2870120) (← links)
- Proofs and Reconstructions (Q2964467) (← links)
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners) (Q3058454) (← links)
- (Q3075241) (← links)
- Interacting with Modal Logics in the Coq Proof Assistant (Q3194730) (← links)
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← links)
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics (Q3455772) (← links)
- A realizability interpretation of Church's simple theory of types (Q4593235) (← links)
- Theorem Provers For Every Normal Modal Logic (Q4645724) (← links)
- Deep Network Guided Proof Search (Q4645728) (← links)
- TacticToe: Learning to Reason with HOL4 Tactics (Q4645730) (← links)
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic (Q4978553) (← links)
- (Q4989394) (← links)
- (Q5028439) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- The CADE-26 automated theorem proving system competition – CASC-26 (Q5145427) (← links)