Satallax
From MaRDI portal
Cited in
(only showing first 100 items - show all)- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- The higher-order prover Leo-III
- scientific article; zbMATH DE number 7178360 (Why is no real title available?)
- On logic embeddings and Gödel's God
- Hammering towards QED
- Theorem provers for every normal modal logic
- A Knuth-Bendix-like ordering for orienting combinator equations
- Functions-as-constructors Higher-order Unification
- TacticToe: learning to reason with HOL4 tactics
- Interacting with Modal Logics in the Coq Proof Assistant
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Restricted combinatory unification
- Verifying the modal logic cube is an easy task (for higher-order automated reasoners)
- Extending Sledgehammer with SMT solvers
- Lash 1.0 (system description)
- Improving automation for higher-order proof steps
- A realizability interpretation of Church's simple theory of types
- Embedding and automating conditional logics in classical higher-order logic
- Superposition with lambdas
- 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
- Cut-elimination for quantified conditional logic
- HOL Based First-Order Modal Logic Provers
- Extensional higher-order paramodulation in Leo-III
- Functions-as-constructors higher-order unification: extended pattern unification
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- 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
- Combining and automating classical and non-classical logics in classical higher-order logics
- A combinator-based superposition calculus for higher-order logic
- Internal guidance for Satallax
- Making higher-order superposition work
- Superposition with lambdas
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- Effective normalization techniques for HOL
- Reducing higher-order theorem proving to a sequence of SAT problems
- Monte Carlo tableau proof search
- scientific article; zbMATH DE number 7471678 (Why is no real title available?)
- 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
- Sqrt_Babylonian
- Zipperposition
- Adimen-SUMO
- Metis
- GRUNGE: a grand unified ATP challenge
- Theorem proving in large formal mathematics as an emerging AI field
- Limited second-order functionality in a first-order setting
- Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
- Making higher-order superposition work
- Superposition for -free higher-order logic
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
This page was built for software: Satallax
