Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint

• URL: http://arxiv.org/abs/2305.15382v1
• Date: Wed, 24 May 2023 17:40:54 GMT
• Title: Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
• Abstract summary: Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a theorem prover for DHOL.

Related papers

• Code as Representation: A Compilable Parsing Paradigm for Academic Documents [50.40789738182074]
  Compilable Academic Document Parsing (CADP) is a paradigm that reconstructs a full page as contextual La plus executable Python.<n>We introduce CADP-Bench, an expert-verified benchmark of full academic pages containing text and multiple SAE types.<n>Results show that even frontier models still struggle to produce high-fidelity executable reconstructions.
  arXiv  Detail & Related papers  (2026-08-18T09:10:43Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Subtyping in DHOL -- Extended preprint [0.0]
  Recently introduced dependent typed higher-order logic (DHOL) offers compromise between expressiveness and automation support.<n>We leverage this design to extend DHOL with refinement and quotient types.<n>We present the syntax, semantics, and translation to HOL for the extended language.
  arXiv  Detail & Related papers  (2025-07-03T17:59:00Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  Large language models (LLMs) produce uncompilable output because their next-token inference procedure does not model formal aspects of code. We introduce a type-constrained decoding approach that leverages type systems to guide code generation. Our approach reduces compilation errors by more than half and increases functional correctness in code synthesis, translation, and repair tasks.
  arXiv  Detail & Related papers  (2025-04-12T15:03:00Z)
• Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts [1.104960878651584]
  Subtyping, also known as subtype polymorphism, is a concept extensively studied in programming language theory. In this paper, we explore the capability of order-sorted logic for utilizing these ideas in the context of Knowledge Representation.
  arXiv  Detail & Related papers  (2025-02-13T11:51:22Z)
• Experiments with Choice in Dependently-Typed Higher-Order Logic [3.072340427031969]
  We extend the DHOL term structure by Hilbert's indefinite choice operator $epsilon$. We define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL. We evaluate the extended translation on a set of dependent HOL problems that require choice.
  arXiv  Detail & Related papers  (2024-10-11T14:49:45Z)
• SAIL: Self-Improving Efficient Online Alignment of Large Language Models [56.59644677997827]
  Reinforcement Learning from Human Feedback is a key method for aligning large language models with human preferences. Recent literature has focused on designing online RLHF methods but still lacks a unified conceptual formulation. Our approach significantly improves alignment performance on open-sourced datasets with minimal computational overhead.
  arXiv  Detail & Related papers  (2024-06-21T18:05:35Z)
• Beyond Prototypes: Semantic Anchor Regularization for Better Representation Learning [82.29761875805369]
  One of the ultimate goals of representation learning is to achieve compactness within a class and well-separability between classes. We propose a novel perspective to use pre-defined class anchors serving as feature centroid to unidirectionally guide feature learning. The proposed Semantic Anchor Regularization (SAR) can be used in a plug-and-play manner in the existing models.
  arXiv  Detail & Related papers  (2023-12-19T05:52:38Z)
• Interpretability at Scale: Identifying Causal Mechanisms in Alpaca [62.65877150123775]
  We use Boundless DAS to efficiently search for interpretable causal structure in large language models while they follow instructions. Our findings mark a first step toward faithfully understanding the inner-workings of our ever-growing and most widely deployed language models.
  arXiv  Detail & Related papers  (2023-05-15T17:15:40Z)
• METGEN: A Module-Based Entailment Tree Generation Framework for Answer Explanation [59.33241627273023]
  We propose METGEN, a Module-based Entailment Tree GEN framework that has multiple modules and a reasoning controller. Given a question, METGEN can iteratively generate the entailment tree by conducting single-step entailment with separate modules and selecting the reasoning flow with the controller. Experiment results show that METGEN can outperform previous state-of-the-art models with only 9% of the parameters.
  arXiv  Detail & Related papers  (2022-05-05T12:06:02Z)
• A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems [0.0]
  We introduce a formal meta-language for probabilistic programming, capable of expressing both programs and the type systems in which they are embedded. We draw on the frameworks of cubical type theory and dependent typed metagraphs to formalize our approach.
  arXiv  Detail & Related papers  (2022-03-30T01:07:37Z)
• Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs [2.28438857884398]
  We show that type checking is able to prune large parts of the hypothesis space of programs. We are able to infer polymorphic types of synthesized clauses and of entire programs.
  arXiv  Detail & Related papers  (2021-02-18T13:40:16Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)
• Plausible Reasoning about EL-Ontologies using Concept Interpolation [27.314325986689752]
  We propose an inductive mechanism which is based on a clear model-theoretic semantics, and can thus be tightly integrated with standard deductive reasoning. We focus on inference, a powerful commonsense reasoning mechanism which is closely related to cognitive models of category-based induction.
  arXiv  Detail & Related papers  (2020-06-25T14:19:41Z)
• Superposition for Lambda-Free Higher-Order Logic [62.997667081978825]
  We introduce refutationally complete superposition calculi for intentional and extensional clausal $lambda$-free higher-order logic. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $lambda$-free higher-order lexicographic path and Knuth-Bendix orders.
  arXiv  Detail & Related papers  (2020-05-05T12:10:21Z)
• The Imandra Automated Reasoning System (system description) [0.0]
  Imandra is a modern computational logic theorem prover. It bridges the gap between decision procedures like SMT and inductive provers like ACL2. Imandra has novel features supporting large-scale industrial applications.
  arXiv  Detail & Related papers  (2020-04-21T19:57:34Z)

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

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.