Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving

• URL: http://arxiv.org/abs/2209.12592v1
• Date: Mon, 26 Sep 2022 11:23:17 GMT
• Title: Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving
• Authors: Christoph Wernhard
• Abstract summary: We introduce here this "combinator term as proof structure" approach to automated first-order proving. The approach builds on a term view of proof structures rooted in condensed detachment and the connection method.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Representing a proof tree by a combinator term that reduces to the tree lets subtle forms of duplication within the tree materialize as duplicated subterms of the combinator term. In a DAG representation of the combinator term these straightforwardly factor into shared subgraphs. To search for proofs, combinator terms can be enumerated, like clausal tableaux, interwoven with unification of formulas that are associated with nodes of the enumerated structures. To restrict the search space, the enumeration can be based on proof schemas defined as parameterized combinator terms. We introduce here this "combinator term as proof structure" approach to automated first-order proving, present an implementation and first experimental results. The approach builds on a term view of proof structures rooted in condensed detachment and the connection method. It realizes features known from the connection structure calculus, which has not been implemented so far.

Related papers

• Integrating Hierarchical Semantic into Iterative Generation Model for Entailment Tree Explanation [7.5496857647335585]
  We propose an architecture of integrating the Hierarchical Semantics of sentences under the framework of Controller-Generator (HiSCG) to explain answers. The proposed method achieves comparable performance on all three settings of the EntailmentBank dataset.
  arXiv  Detail & Related papers  (2024-09-26T11:46:58Z)
• Approximate learning of parsimonious Bayesian context trees [0.0]
  The proposed framework is tested on synthetic and real-world data examples. It outperforms existing sequence models when fitted to real protein sequences and honeypot computer terminal sessions.
  arXiv  Detail & Related papers  (2024-07-27T11:50:40Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models. A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters. We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
  arXiv  Detail & Related papers  (2023-10-05T07:10:40Z)
• Interpretable Sequence Clustering [3.280979689839737]
  We propose a method called Interpretable Sequence Clustering Tree (ISCT) ISCT generates k leaf nodes, corresponding to k clusters, which provides an intuitive explanation on how each cluster is formed. Experimental results on 14 real-world data sets demonstrate that our proposed method provides an interpretable tree structure.
  arXiv  Detail & Related papers  (2023-09-03T11:31:44Z)
• Range-Restricted Interpolation through Clausal Tableaux [0.0]
  We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig in first-order logic. The proof system is clausal tableaux, which stems from first-order ATP.
  arXiv  Detail & Related papers  (2023-06-06T10:42: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)
• Compositional Generalization Requires Compositional Parsers [69.77216620997305]
  We compare sequence-to-sequence models and models guided by compositional principles on the recent COGS corpus. We show structural generalization is a key measure of compositional generalization and requires models that are aware of complex structure.
  arXiv  Detail & Related papers  (2022-02-24T07:36:35Z)
• A convergent inflation hierarchy for quantum causal structures [1.6758573326215689]
  A causal structure is a description of the functional dependencies between random variables. Inflation techniques associate causal structures to a hierarchy of increasingly strict compatibility tests. In this paper, we construct a first version of the quantum inflation hierarchy that is provably convergent.
  arXiv  Detail & Related papers  (2021-10-27T18:00:02Z)
• Complex Event Forecasting with Prediction Suffix Trees: Extended Technical Report [70.7321040534471]
  Complex Event Recognition (CER) systems have become popular in the past two decades due to their ability to "instantly" detect patterns on real-time streams of events. There is a lack of methods for forecasting when a pattern might occur before such an occurrence is actually detected by a CER engine. We present a formal framework that attempts to address the issue of Complex Event Forecasting.
  arXiv  Detail & Related papers  (2021-09-01T09:52:31Z)
• Fold2Seq: A Joint Sequence(1D)-Fold(3D) Embedding-based Generative Model for Protein Design [70.27706384570723]
  We propose Fold2Seq, a novel framework for designing protein sequences conditioned on a specific target fold. We show improved or comparable performance of Fold2Seq in terms of speed, coverage, and reliability for sequence design. The unique advantages of fold-based Fold2Seq, in comparison to a structure-based deep model and RosettaDesign, become more evident on three additional real-world challenges.
  arXiv  Detail & Related papers  (2021-06-24T14:34:24Z)
• Span-based Semantic Parsing for Compositional Generalization [53.24255235340056]
  SpanBasedSP predicts a span tree over an input utterance, explicitly encoding how partial programs compose over spans in the input. On GeoQuery, SCAN and CLOSURE, SpanBasedSP performs similarly to strong seq2seq baselines on random splits, but dramatically improves performance compared to baselines on splits that require compositional generalization.
  arXiv  Detail & Related papers  (2020-09-13T16:42:18Z)

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.