Related papers: Teaching Higher-Order Logic Using Isabelle

Teaching Higher-Order Logic Using Isabelle

URL: http://arxiv.org/abs/2404.05458v1
Date: Mon, 8 Apr 2024 12:40:27 GMT
Title: Teaching Higher-Order Logic Using Isabelle
Authors: Simon Tobias Lund, Jørgen Villadsen,
Abstract summary: We present a formalization of higher-order logic in the Isabelle proof assistant. It should serve as a good introduction for someone looking into learning about higher-order logic and proof assistants.
Score: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We present a formalization of higher-order logic in the Isabelle proof assistant, building directly on the foundational framework Isabelle/Pure and developed to be as small and readable as possible. It should therefore serve as a good introduction for someone looking into learning about higher-order logic and proof assistants, without having to study the much more complex Isabelle/HOL with heavier automation. To showcase our development and approach we explain a sample proof, describe the axioms and rules of our higher-order logic, and discuss our experience with teaching the subject in a classroom setting.

Related papers

Exploring the Role of Reasoning Structures for Constructing Proofs in Multi-Step Natural Language Reasoning with Large Language Models [30.09120709652445]
This paper is centred around a focused study: whether the current state-of-the-art generalist LLMs can leverage the structures in a few examples to better construct the proof structures with textitin-context learning.
arXiv Detail & Related papers (2024-10-11T00:45:50Z)
Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
We propose a complex reasoning schema over KG upon large language models (LLMs) We augment the arbitrary first-order logical queries via binary tree decomposition to stimulate the reasoning capability of LLMs. Experiments across widely used datasets demonstrate that LACT has substantial improvements(brings an average +5.5% MRR score) over advanced methods.
arXiv Detail & Related papers (2024-05-02T18:12:08Z)
LogicBench: Towards Systematic Evaluation of Logical Reasoning Ability of Large Language Models [52.03659714625452]
Recently developed large language models (LLMs) have been shown to perform remarkably well on a wide range of language understanding tasks. But, can they really "reason" over the natural language? This question has been receiving significant research attention and many reasoning skills such as commonsense, numerical, and qualitative have been studied.
arXiv Detail & Related papers (2024-04-23T21:08:49Z)
Logic-Scaffolding: Personalized Aspect-Instructed Recommendation Explanation Generation using LLMs [20.446594942586604]
We propose a framework called Logic-Scaffolding, that combines the ideas of aspect-based explanation and chain-of-thought prompting to generate explanations through intermediate reasoning steps. In this paper, we share our experience in building the framework and present an interactive demonstration for exploring our results.
arXiv Detail & Related papers (2023-12-22T00:30:10Z)
An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
This approach allows for the computer-assisted analysis of abstract dialectical frameworks. Exemplary applications include the formal analysis and verification of meta-theoretical properties.
arXiv Detail & Related papers (2023-12-08T09:32:26Z)
Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
We propose a structure-modeled textual encoding framework for inductive logical reasoning over KGs. It encodes linearized query structures and entities using pre-trained language models to find answers. We conduct experiments on two inductive logical reasoning datasets and three transductive datasets.
arXiv Detail & Related papers (2023-05-23T01:25:29Z)
On Exams with the Isabelle Proof Assistant [0.0]
We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems and understanding of proofs in the higher-order logic of Isabelle/HOL.
arXiv Detail & Related papers (2023-03-10T11:37:09Z)
elBERto: Self-supervised Commonsense Learning for Question Answering [131.51059870970616]
We propose a Self-supervised Bidirectional Representation Learning of Commonsense framework, which is compatible with off-the-shelf QA model architectures. The framework comprises five self-supervised tasks to force the model to fully exploit the additional training signals from contexts containing rich commonsense. elBERto achieves substantial improvements on out-of-paragraph and no-effect questions where simple lexical similarity comparison does not help.
arXiv Detail & Related papers (2022-03-17T16:23:45Z)
New Algebraic Normative Theories for Ethical and Legal Reasoning in the LogiKEy Framework [0.0]
We introduce LogiKEy methodology based on semantical embedding of deontic logics into classic higher-order logic. We considerably extend the LogiKEy deontic logics and dataset using an algebraic approach.
arXiv Detail & Related papers (2021-07-25T16:33:07Z)
Logic-Driven Context Extension and Data Augmentation for Logical Reasoning of Text [65.24325614642223]
We propose to understand logical symbols and expressions in the text to arrive at the answer. Based on such logical information, we put forward a context extension framework and a data augmentation algorithm. Our method achieves the state-of-the-art performance, and both logic-driven context extension framework and data augmentation algorithm can help improve the accuracy.
arXiv Detail & Related papers (2021-05-08T10:09:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.