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

DOI10.1007/978-3-319-20615-8_22zbMATH Open1417.68196arXiv1505.01629OpenAlexW2963739488MaRDI QIDQ3453128FDOQ3453128

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)

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.

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

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

Mathematics Subject Classification ID

Knowledge representation (68T30)

Cites Work

• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• 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)
• \(\Omega\)-ANTS -- An open approach at combining interactive and automated theorem proving
• Social choice and individual values
• Extending Sledgehammer with SMT solvers
• Title not available (Why is that?)
• Title not available (Why is that?)
• Combined reasoning by automated cooperation
• Title not available (Why is that?)
• Term indexing
• Explicit substitutions
• Introduction to generalized type systems
• A Linear Spine Calculus
• A taxonomy of parallel strategies for deduction
• Alpha-conversion and typability

Cited In (5)

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

Uses Software

• LEO-II
• TPTP
• Satallax
• Twelf
• Sledgehammer
• Abella
• Leo-III
• Leo
• 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)