Satallax
From MaRDI portal
Cited in
(only showing first 100 items - show all)- LEO-II
- Nitpick
- TPS
- RuleML
- THF0
- Paradox
- SPASS
- TPTP
- Metis
- Algorithm and tools for constructing canonical forms of linear semi-algebraic formulas
- Superposition for -free higher-order logic
- The higher-order prover Leo-III
- ETPS
- SCOTT
- Sledgehammer
- Embedding and automating conditional logics in classical higher-order logic
- LEO-II and Satallax on the Sledgehammer test bench
- StarExec
- A Knuth-Bendix-like ordering for orienting combinator equations
- A combinator-based superposition calculus for higher-order logic
- Lash 1.0 (system description)
- Functions-as-constructors higher-order unification: extended pattern unification
- leanCoP
- ileanCoP
- Minlog
- Equinox
- QMLTP
- E Theorem Prover
- SystemOnTPTP
- Automating free logic in HOL, with an experimental application in category theory
- Limited second-order functionality in a first-order setting
- Extending SMT solvers to higher-order logic
- Restricted combinatory unification
- GRUNGE: a grand unified ATP challenge
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- HOLyHammer
- Reducing higher-order theorem proving to a sequence of SAT problems
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Cut-elimination for quantified conditional logic
- MetTeL
- GQML
- Scavenger 0.1: a theorem prover based on conflict resolution
- Monte Carlo tableau proof search
- AgsyHOL
- HOT
- LeoPARD
- Beagle
- FOOL
- Extensional higher-order paramodulation in Leo-III
- On logic embeddings and Gödel's God
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Internal guidance for Satallax
- Effective normalization techniques for HOL
- Agent-based HOL reasoning
- MaLeS: a framework for automatic tuning of automated theorem provers
- HOL Based First-Order Modal Logic Provers
- The higher-order prover \textsc{Leo}-II
- Semi-intelligible Isar proofs from machine-generated proofs
- MSPASS
- Proofs and reconstructions
- Leo-III
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- Leo
- DISCOUNT
- Interacting with Modal Logics in the Coq Proof Assistant
- Teyjus
- MleanCoP
- FMLtoHOL
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
- Scavenger
- embed_modal
- Lambda Free RPOs
- CoqHammer
- Robbins Conjecture
- Network Security Policy Verification
- Sqrt_Babylonian
- AxiomaticCategoryTheory
- GoedelGod
- Regular_Algebras
- Zipperposition
- A realizability interpretation of Church's simple theory of types
- Theorem provers for every normal modal logic
- Deep network guided proof search
- TacticToe: learning to reason with HOL4 tactics
- Theorem proving in large formal mathematics as an emerging AI field
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Superposition for lambda-free higher-order logic
- Efficient full higher-order unification
- Practical Proof Search for Coq by Type Inhabitation
- The CADE-26 automated theorem proving system competition -- CASC-26
- Adimen-SUMO
- Hammering towards QED
- Extending Sledgehammer with SMT solvers
- Reducing higher-order theorem proving to a sequence of SAT problems
- scientific article; zbMATH DE number 7178360 (Why is no real title available?)
- Computer-assisted analysis of the Anderson-Hájek ontological controversy
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- Functions-as-constructors Higher-order Unification
This page was built for software: Satallax
