Satallax
From MaRDI portal
Software:18920
swMATH6849MaRDI QIDQ18920FDOQ18920
Author name not available (Why is that?)
Cited In (62)
- Making higher-order superposition work
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Title not available (Why is that?)
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Restricted combinatory unification
- 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
- Scavenger 0.1: a theorem prover based on conflict resolution
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Agent-Based HOL Reasoning
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- 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?)
- Title not available (Why is that?)
- 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
- Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)
- Analytic Tableaux for Higher-Order Logic with Choice
- 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
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Title not available (Why is that?)
- Reducing higher-order theorem proving to a sequence of SAT problems
- Monte Carlo tableau proof search
- Theorem Provers For Every Normal Modal Logic
- TacticToe: Learning to Reason with HOL4 Tactics
- GRUNGE: a grand unified ATP challenge
- Proofs and Reconstructions
- Extending Sledgehammer with SMT Solvers
- Internal Guidance for Satallax
- Limited second-order functionality in a first-order setting
- Superposition for \(\lambda\)-free higher-order logic
- 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-26 automated theorem proving system competition – CASC-26
- Extending SMT solvers to higher-order logic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Practical Proof Search for Coq by Type Inhabitation
- Deep Network Guided Proof Search
- Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems
- Automating free logic in HOL, with an experimental application in category theory
- On Logic Embeddings and Gödel’s God
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- LEO-II and Satallax on the Sledgehammer test bench
- The higher-order prover Leo-III
- Hammering towards QED
- Functions-as-constructors Higher-order Unification
- A Knuth-Bendix-like ordering for orienting combinator equations
- Interacting with Modal Logics in the Coq Proof Assistant
This page was built for software: Satallax
