Satallax
From MaRDI portal
swMATH6849MaRDI QIDQ18920FDOQ18920
Author name not available (Why is that?)
Official website: http://www.ps.uni-saarland.de/~cebrown/satallax/
Cited In (only showing first 100 items - show all)
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Lash
- Restricted combinatory unification
- A realizability interpretation of Church's simple theory of types
- Lash 1.0 (system description)
- The CADE-26 automated theorem proving system competition -- CASC-26
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Extensional higher-order paramodulation in Leo-III
- Proofs and reconstructions
- Reducing higher-order theorem proving to a sequence of SAT problems
- Making higher-order superposition work
- Effective normalization techniques for HOL
- GRUNGE: a grand unified ATP challenge
- Making higher-order superposition work
- Limited second-order functionality in a first-order setting
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Automating free logic in HOL, with an experimental application in category theory
- Agent-based HOL reasoning
- Title not available (Why is that?)
- Functions-as-constructors Higher-order Unification
- A Knuth-Bendix-like ordering for orienting combinator equations
- Extending Sledgehammer with SMT solvers
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Superposition with lambdas
- 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
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- HOL Based First-Order Modal Logic Provers
- Cut-elimination for quantified conditional logic
- 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
- Deep network guided proof search
- Analytic tableaux for higher-order logic with choice
- 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}\)
- Title not available (Why is that?)
- Reducing higher-order theorem proving to a sequence of SAT problems
- Monte Carlo tableau proof search
- LEO-II
- Nitpick
- TPS
- RuleML
- Paradox
- THF0
- SPASS
- TPTP
- ETPS
- SCOTT
- Sledgehammer
- StarExec
- Equinox
- ileanCoP
- leanCoP
- Minlog
- QMLTP
- E Theorem Prover
- SystemOnTPTP
- HOLyHammer
- GQML
- MetTeL
- AgsyHOL
- HOT
- Beagle
- LeoPARD
- FOOL
- MSPASS
- Leo-III
- DISCOUNT
- Leo
- FMLtoHOL
- MleanCoP
- Teyjus
- Scavenger
- embed_modal
- Lambda Free RPOs
- CoqHammer
- Robbins Conjecture
- AxiomaticCategoryTheory
- GoedelGod
- Network Security Policy Verification
- Regular_Algebras
- Theorem proving in large formal mathematics as an emerging AI field
- Sqrt_Babylonian
- Zipperposition
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- Superposition for \(\lambda\)-free higher-order logic
- Adimen-SUMO
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Extending SMT solvers to higher-order logic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Practical Proof Search for Coq by Type Inhabitation
This page was built for software: Satallax