Agent-Based HOL Reasoning

DOI10.1007/978-3-319-42432-3_10zbMath1434.68646OpenAlexW2487610225MaRDI QIDQ2819202

Christoph Benzmüller, Max Wisniewski, Alexander Steen

Publication date: 28 September 2016

Published in: Mathematical Software – ICMS 2016 (Search for Journal in Brave)

Full work available at URL: http://orbilu.uni.lu/handle/10993/40843

zbMATH Keywords

reasoninghigher-order logicautomated theorem provingnonclassical logics

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Extensional higher-order paramodulation in Leo-III ⋮ Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support ⋮ The CADE-26 automated theorem proving system competition – CASC-26

Uses Software

• Isabelle/HOL
• TPTP
• HOL
• Satallax
• LeoPARD
• Leo-III

Cites Work

• Unnamed Item
• The higher-order prover \textsc{Leo}-II
• Lightweight relevance filtering for machine-generated resolution problems
• Isabelle/HOL. A proof assistant for higher-order logic
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Effective Normalization Techniques for HOL
• Computational Aspects of Cooperative Game Theory
• Satallax: An Automatic Higher-Order Prover
• LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Higher-order semantics and extensionality
• A formulation of the simple theory of types
• Completeness in the theory of types

This page was built for publication: Agent-Based HOL Reasoning