\textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners

DOI10.1007/978-3-319-20615-8_22MaRDI QIDQ3453128zbMATH OpenOpenAlexFDO

Authors Max Wisniewski, Alexander Steen, Christoph Benzmüller

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)

Abstract: LeoPARD supports the implementation of knowledge representation and reasoning tools for higher-order logic(s). It combines a sophisticated data structure layer (polymorphically typed {lambda}-calculus with nameless spine notation, explicit substitutions, and perfect term sharing) with an ambitious multi-agent blackboard architecture (supporting prover parallelism at the term, clause, and search level). Further features of LeoPARD include a parser for all TPTP dialects, a command line interpreter, and generic means for the integration of external reasoners.

Recommendations

• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• The higher-order prover \textsc{Leo}-II
• The higher-order prover Leo-III
• Extensional higher-order paramodulation in Leo-III
• Agent-based HOL reasoning

Cites work

• -ANTS -- An open approach at combining interactive and automated theorem proving
• A Linear Spine Calculus
• A taxonomy of parallel strategies for deduction
• Alpha-conversion and typability
• Combined reasoning by automated cooperation
• Explicit substitutions
• Extending Sledgehammer with SMT solvers
• scientific article; zbMATH DE number 5850137 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Introduction to generalized type systems
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Satallax: An Automatic Higher-Order Prover
• Social choice and individual values
• Term indexing
• The Abella Interactive Theorem Prover (System Description)
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Cited in

(7)

• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
• LeoPARD
• Extensional higher-order paramodulation in Leo-III
• Automating free logic in Isabelle/HOL
• Agent-based HOL reasoning
• Gödel's God in Isabelle/HOL
• Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL

Describes a project that uses

Uses Software

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

This page was built for publication: \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453128)