Experiments with Choice in Dependently-Typed Higher-Order Logic

• URL: http://arxiv.org/abs/2410.08874v1
• Date: Fri, 11 Oct 2024 14:49:45 GMT
• Title: Experiments with Choice in Dependently-Typed Higher-Order Logic
• Abstract summary: 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.
• Score: 3.072340427031969
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice can be added to DHOL. We extend the DHOL term structure by Hilbert's indefinite choice operator $\epsilon$, define a translation of the choice terms to HOL choice that extends the existing translation from DHOL to HOL and show that the extension of the translation is complete and give an argument for soundness. We finally evaluate the extended translation on a set of dependent HOL problems that require choice.

Related papers

• A Data-Efficient Path to Multilingual LLMs: Language Expansion via Post-training PARAM$Δ$ Integration into Upcycled MoE [61.0405668388095]
  We introduce method, which upcycles a dense model into a Mixture-of-Experts(MoE) architecture, allocating different experts to different languages.<n>Experiments demonstrate method's superiority even against baselines with similar FLOPs or number of parameters.
  arXiv  Detail & Related papers  (2026-05-18T08:59:08Z)
• Job Skill Extraction via LLM-Centric Multi-Module Framework [51.37063712967151]
  We present SRICL, an LLM-centric framework that combines semantic retrieval, in-context learning, and supervised fine-tuning.<n>On six public span-labeled corpora of job-ad sentences, SRICL achieves substantial STRICT-F1 improvements over GPT-3.5 prompting baselines and sharply reduces invalid tags and hallucinated spans.
  arXiv  Detail & Related papers  (2026-04-23T10:46:07Z)
• 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)
• Intensional FOL: Many-Sorted Extension [0.0]
  The concepts used in IFOL have associated to them a list of sorted attributes, and the sorts are the intensional concepts as well. The requirement to extend the unsorted IFOL (Intensional FOL) to many-sorted IFOL is mainly based on the fact that a natural language is implicitly many-sorted.
  arXiv  Detail & Related papers  (2024-09-03T19:50:57Z)
• Multilingual Contrastive Decoding via Language-Agnostic Layers Skipping [60.458273797431836]
  Decoding by contrasting layers (DoLa) is designed to improve the generation quality of large language models. We find that this approach does not work well on non-English tasks. Inspired by previous interpretability work on language transition during the model's forward pass, we propose an improved contrastive decoding algorithm.
  arXiv  Detail & Related papers  (2024-07-15T15:14:01Z)
• Towards Effective Disambiguation for Machine Translation with Large Language Models [65.80775710657672]
  We study the capabilities of large language models to translate "ambiguous sentences" Experiments show that our methods can match or outperform state-of-the-art systems such as DeepL and NLLB in four out of five language directions.
  arXiv  Detail & Related papers  (2023-09-20T22:22:52Z)
• Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint [0.0]
  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.
  arXiv  Detail & Related papers  (2023-05-24T17:40:54Z)
• FOLIO: Natural Language Reasoning with First-Order Logic [147.50480350846726]
  We present FOLIO, a human-annotated, logically complex and diverse dataset for reasoning in natural language (NL) FOLIO consists of 1,430 examples (unique conclusions), each paired with one of 487 sets of premises used to deductively reason for the validity of each conclusion. For both NL reasoning and NL-FOL translation, we benchmark multiple state-of-the-art language models.
  arXiv  Detail & Related papers  (2022-09-02T06:50:11Z)
• A unified logical framework for explanations in classifier systems [10.256904719009471]
  We present a modal language of a ceteris paribus nature which supports reasoning about binary input classifiers and their properties. We study a family of models, axiomatize it as two proof systems regarding the cardinality of the language and show completeness of our axiomatics. We leverage the language to formalize counterfactual conditional as well as a variety of notions of explanation including abductive, contrastive and counterfactual explanations.
  arXiv  Detail & Related papers  (2021-05-30T07:49:56Z)
• Superposition with Lambdas [59.87497175616048]
  We design a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $betaeta$-equivalence classes of $lambda$-terms and rely on higher-order unification to achieve refutational completeness.
  arXiv  Detail & Related papers  (2021-01-31T13:53:17Z)
• Proof-theoretic aspects of NL$\lambda$ [0.0]
  We present a proof-theoretic analysis of the logic NL$lambda$. We introduce a novel calculus of proof nets and prove it is sound and complete with respect to the sequent calculus for the logic. We show there is an unexpected convergence of the natural language analyses proposed in the two formalisms.
  arXiv  Detail & Related papers  (2020-10-23T08:13:39Z)
• Constructing a Family Tree of Ten Indo-European Languages with Delexicalized Cross-linguistic Transfer Patterns [57.86480614673034]
  We formalize the delexicalized transfer as interpretable tree-to-string and tree-to-tree patterns. This allows us to quantitatively probe cross-linguistic transfer and extend inquiries of Second Language Acquisition.
  arXiv  Detail & Related papers  (2020-07-17T15:56:54Z)
• 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)

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.