LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners

DOI10.1007/978-3-319-20615-8_22zbMath1417.68196arXiv1505.01629OpenAlexW2963739488MaRDI QIDQ3453128

Max Wisniewski, Christoph Benzmüller, Alexander Steen

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1505.01629

Mathematics Subject Classification ID

Knowledge representation (68T30)

Related Items

Extensional higher-order paramodulation in Leo-III, Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support, Automating Free Logic in Isabelle/HOL, Agent-Based HOL Reasoning, LeoPARD

Uses Software

• LEO-II
• TPTP
• Satallax
• Twelf
• Sledgehammer
• Abella
• Leo-III
• Leo
• Teyjus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combined reasoning by automated cooperation
• A taxonomy of parallel strategies for deduction
• Alpha-conversion and typability
• Extending Sledgehammer with SMT solvers
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Satallax: An Automatic Higher-Order Prover
• The Abella Interactive Theorem Prover (System Description)
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• A Linear Spine Calculus
• Explicit substitutions
• Introduction to generalized type systems