Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory

• URL: http://arxiv.org/abs/2004.07390v1
• Date: Wed, 15 Apr 2020 23:26:04 GMT
• Title: Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
• Authors: Dominik Kirst and Dominique Larchey-Wendling
• Abstract summary: We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. We give a full classification of FSAT depending on the first-order signature of non-logical symbols. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability proofs.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on the first-order signature of non-logical symbols. On the one hand, our development focuses on Trakhtenbrot's theorem, stating that FSAT is undecidable as soon as the signature contains an at least binary relation symbol. Our proof proceeds by a many-one reduction chain starting from the Post correspondence problem. On the other hand, we establish the decidability of FSAT for monadic first-order logic, i.e. where the signature only contains at most unary function and relation symbols, as well as the enumerability of FSAT for arbitrary enumerable signatures. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability proofs.

Related papers

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation. For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• Faithful Logical Reasoning via Symbolic Chain-of-Thought [39.94884827166363]
  We propose SymbCoT, a framework that integrates symbolic expressions and logic rules with Chain-of-Thought prompting. We show that SymbCoT shows striking improvements over the CoT method consistently. This is the first to combine symbolic expressions and rules into CoT for logical reasoning with LLMs.
  arXiv  Detail & Related papers  (2024-05-28T16:55:33Z)
• Mitigating Misleading Chain-of-Thought Reasoning with Selective Filtering [59.495717939664246]
  Large language models have manifested remarkable capabilities by leveraging chain-of-thought (CoT) reasoning techniques to solve intricate questions. We propose a novel approach called the selective filtering reasoner (SelF-Reasoner) that assesses the entailment relationship between the question and the candidate reasoning chain. SelF-Reasoner improves the fine-tuned T5 baseline consistently over the ScienceQA, ECQA, and LastLetter tasks.
  arXiv  Detail & Related papers  (2024-03-28T06:28:35Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)
• Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions [0.0]
  We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions. As usual in synthetic approaches, we employ a definition of oracle computations based on meta-level functions. We show that Turing reducibility forms an upper semilattice, transports decidability, and is strictly more expressive than truth-table reducibility.
  arXiv  Detail & Related papers  (2023-07-28T13:16:46Z)
• Beyond Chain-of-Thought, Effective Graph-of-Thought Reasoning in Language Models [74.40196814292426]
  We propose Graph-of-Thought (GoT) reasoning, which models human thought processes not only as a chain but also as a graph. GoT captures the non-sequential nature of human thinking and allows for a more realistic modeling of thought processes. We evaluate GoT's performance on a text-only reasoning task and a multimodal reasoning task.
  arXiv  Detail & Related papers  (2023-05-26T02:15:09Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
  arXiv  Detail & Related papers  (2023-05-20T11:26:51Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens [0.7614628596146599]
  We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. We give a full classification of FSAT depending on the first-order signature of non-logical symbols. All our results are mechanised in the framework of a growing Coq library of synthetic undecidability.
  arXiv  Detail & Related papers  (2021-04-29T16:05:31Z)
• 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)

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.