LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)

TL;DR

This workshop focuses on practical advancements and discussions in automated reasoning within higher-order logic, emphasizing proof systems, tools, and digital proof libraries to enhance reasoning capabilities.

Contribution

It consolidates recent developments, fosters collaboration, and discusses the development of higher-order reasoning systems and their practical strengths.

Findings

Development of proof assistants for higher-order logic

Comparative analysis of automated higher-order reasoning systems

Proposals for a higher-order TPTP database

Abstract

This workshop brings together practioners and researchers who are involved in the everyday aspects of logical systems based on higher-order logic. We hope to create a friendly and highly interactive setting for discussions around the following four topics. Implementation and development of proof assistants based on any notion of impredicativity, automated theorem proving tools for higher-order logic reasoning systems, logical framework technology for the representation of proofs in higher-order logic, formal digital libraries for storing, maintaining and querying databases of proofs. We envision attendees that are interested in fostering the development and visibility of reasoning systems for higher-order logics. We are particularly interested in a discusssion on the development of a higher-order version of the TPTP and in comparisons of the practical strengths of automated higher-order reasoning systems. Additionally, the workshop includes system demonstrations. ESHOL is the successor of the ESCAR and ESFOR workshops held at CADE 2005 and IJCAR 2004.