Agent-based HOL reasoning

DOI10.1007/978-3-319-42432-3_10MaRDI QIDQ2819202zbMATH OpenOpenAlexFDO

Authors Alexander Steen, Max Wisniewski, Christoph Benzmüller

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

automated theorem provinghigher-order logicnonclassical logicsreasoning

Mathematics Subject Classification ID

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

Recommendations

• Extensional higher-order paramodulation in Leo-III
• scientific article; zbMATH DE number 1882065
• Extensional paramodulation for higher-order logic and its effective implementation Leo-III
• scientific article; zbMATH DE number 1497751
• \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners

Cites work

• \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
• A formulation of the simple theory of types
• Completeness in the theory of types
• Computational Aspects of Cooperative Game Theory
• Effective normalization techniques for HOL
• Higher-order semantics and extensionality
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics
• Isabelle/HOL. A proof assistant for higher-order logic
• Lightweight relevance filtering for machine-generated resolution problems
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Satallax: An Automatic Higher-Order Prover
• The higher-order prover \textsc{Leo}-II
• 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
• Extensional higher-order paramodulation in Leo-III
• \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
• scientific article; zbMATH DE number 1497751 (Why is no real title available?)
• scientific article; zbMATH DE number 1773056 (Why is no real title available?)
• scientific article; zbMATH DE number 1882065 (Why is no real title available?)
• The CADE-26 automated theorem proving system competition -- CASC-26

Describes a project that uses

Uses Software

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

This page was built for publication: Agent-based HOL reasoning

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