LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners
LeoPARD - A Generic Platform for the Implementation of Higher-Order Reasoners
复制标题
LeoPARD - 用于实现高阶推理机的通用平台
DOI：
10.1007/978-3-319-20615-8_22
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Christoph Benzmüller
中科院分区：
文献类型：
--
作者：
M. Wisniewski;A. Steen;Christoph Benzmüller
LeoPARD支持高阶逻辑的知识表示和推理工具的实现。它结合了一个复杂的数据结构层（多态类型的{\lambda}-演算与无名的脊柱符号，显式替换，和完美的术语共享）与一个雄心勃勃的多代理黑板架构（支持在术语，子句和搜索级别的证明并行）。LeoPARD的其他特性包括一个用于所有TPTP方言的解析器、一个命令行解释器和用于集成外部推理器的通用方法。
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.
使用 SMT 求解器扩展 Sledgehammer
DOI：
10.1007/s10817-013-9278-5
发表时间：
2013
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jasmin Christian Blanchette;Sascha Böhme;Lawrence C. Paulson
通讯作者：
Lawrence C. Paulson