Trakhtenbrot's Theorem in Coq: Finite Model Theory through the
Constructive Lens
- URL: http://arxiv.org/abs/2104.14445v1
- Date: Thu, 29 Apr 2021 16:05:31 GMT
- Title: Trakhtenbrot's Theorem in Coq: Finite Model Theory through the
Constructive Lens
- 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.
- Score: 0.7614628596146599
- License: http://creativecommons.org/licenses/by/4.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. To showcase an application of Trakthenbrot's theorem, we continue
our reduction chain with a many-one reduction from FSAT to separation logic.
All our results are mechanised in the framework of a growing Coq library of
synthetic undecidability proofs.
Related papers
- 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) - SymBa: Symbolic Backward Chaining for Multi-step Natural Language
Reasoning [6.961946145048321]
We propose SymBa (Symbolic Backward Chaining) to address the limitations of current backward chaining implementations.
In SymBa, the symbolic top-down solver controls the entire proof process and the LLM is called to generate a single reasoning step only when the solver encounters a dead end.
By this novel solver-LLM integration, SymBa achieves significant improvement in performance, proof faithfulness, and efficiency in diverse multi-step reasoning benchmarks.
arXiv Detail & Related papers (2024-02-20T08:27:05Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity.
We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points.
We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
arXiv Detail & Related papers (2024-02-14T05:57:58Z) - 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) - 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) - 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) - 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) - Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model
Theory [0.0]
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.
arXiv Detail & Related papers (2020-04-15T23:26:04Z)
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.