Leo-III
From MaRDI portal
Cited in
(35)- Superposition for -free higher-order logic
- Satallax
- NiVER
- Local is best: efficient reductions to modal logic \textsf{K}
- Lash 1.0 (system description)
- Local reductions for the modal cube
- QMLTP
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Automating free logic in HOL, with an experimental application in category theory
- Restricted combinatory unification
- GRUNGE: a grand unified ATP challenge
- HOT
- LeoPARD
- Extensional higher-order paramodulation in Leo-III
- Effective normalization techniques for HOL
- Agent-based HOL reasoning
- MATHsAiD
- MleanCoP
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- embed_modal
- ZRes
- LegalRuleML
- AxiomaticCategoryTheory
- Zipperposition
- Extensional paramodulation for higher-order logic and its effective implementation Leo-III
- Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
- Practical Proof Search for Coq by Type Inhabitation
- The CADE-26 automated theorem proving system competition -- CASC-26
- Theorema 2.0: computer-assisted natural-style mathematics
- Functions-as-constructors Higher-order Unification
- PLM
- Superposition with lambdas
- LogiKEy
- Axiom Systems for Category Theory in Free Logic
- Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL
This page was built for software: Leo-III
