Superposition with Lambdas

• URL: http://arxiv.org/abs/2102.00453v1
• Date: Sun, 31 Jan 2021 13:53:17 GMT
• Title: Superposition with Lambdas
• Authors: Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirovi\'c, Uwe Waldmann
• Abstract summary: 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.
• Score: 59.87497175616048
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We designed 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 $\beta\eta$-equivalence classes of $\lambda$-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.

Related papers

• Aggregation of Reasoning: A Hierarchical Framework for Enhancing Answer Selection in Large Language Models [84.15513004135576]
  Current research enhances the reasoning performance of Large Language Models (LLMs) by sampling multiple reasoning chains and ensembling based on the answer frequency. This approach fails in scenarios where the correct answers are in the minority. We introduce a hierarchical reasoning aggregation framework AoR, which selects answers based on the evaluation of reasoning chains.
  arXiv  Detail & Related papers  (2024-05-21T17:12:19Z)
• Premise Order Matters in Reasoning with Large Language Models [57.18850969634412]
  We show that large language models (LLMs) are surprisingly brittle to the ordering of the premises. We observe that LLMs achieve the best performance when the premise order aligns with the context required in intermediate reasoning steps.
  arXiv  Detail & Related papers  (2024-02-14T04:50:18Z)
• Higher-Order DisCoCat (Peirce-Lambek-Montague semantics) [0.0]
  We propose a new definition of higher-order DisCoCat (categorical compositional distributional) models. Our models can be seen as a variant of Montague semantics based on a calculus where the primitives act on string diagrams rather than logical formulae.
  arXiv  Detail & Related papers  (2023-11-29T17:04:15Z)
• 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)
• SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning [0.3867363075280543]
  We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with respect to a fixed reduction ordering.
  arXiv  Detail & Related papers  (2023-05-22T11:12:39Z)
• 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)
• Towards Ranking-based Semantics for Abstract Argumentation using Conditional Logic Semantics [8.619759570837951]
  We propose a novel ranking-based semantics for Dung-style argumentation frameworks. Using an intuitive translation for an argumentation framework to generate conditionals, we can apply nonmonotonic inference systems to generate a ranking on possible worlds.
  arXiv  Detail & Related papers  (2020-08-05T08:34:16Z)
• Second-Order Information in Non-Convex Stochastic Optimization: Power and Limitations [54.42518331209581]
  We find an algorithm which finds. epsilon$-approximate stationary point (with $|nabla F(x)|le epsilon$) using. $(epsilon,gamma)$surimate random random points. Our lower bounds here are novel even in the noiseless case.
  arXiv  Detail & Related papers  (2020-06-24T04:41:43Z)
• 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.