Satallax

swMATH6849MaRDI QIDQ18920FDOQ18920

Author name not available (Why is that?)

Official website: http://www.ps.uni-saarland.de/~cebrown/satallax/

Described by source

• Satallax: An Automatic Higher-Order Prover
• Analytic tableaux for higher-order logic with choice

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