Range-Restricted Interpolation through Clausal Tableaux

• URL: http://arxiv.org/abs/2306.03572v3
• Date: Wed, 27 Sep 2023 08:44:07 GMT
• Title: Range-Restricted Interpolation through Clausal Tableaux
• Authors: Christoph Wernhard
• Abstract summary: 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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig interpolation in first-order logic. The proof system is clausal tableaux, which stems from first-order ATP. Our results are induced by a restriction of the clausal tableau structure, which can be achieved in general by a proof transformation, also if the source proof is by resolution/paramodulation. Primarily addressed applications are query synthesis and reformulation with interpolation. Our methodical approach combines operations on proof structures with the immediate perspective of feasible implementation through incorporating highly optimized first-order provers.

Related papers

• Uncertainty Quantification with Bayesian Higher Order ReLU KANs [0.0]
  We introduce the first method of uncertainty quantification in the domain of Kolmogorov-Arnold Networks, specifically focusing on (Higher Order) ReLUKANs. We validate our method through a series of closure tests, including simple one-dimensional functions. We demonstrate the method's ability to correctly identify functional dependencies introduced through the inclusion of a term.
  arXiv  Detail & Related papers  (2024-10-02T15:57:18Z)
• Formally Certified Approximate Model Counting [25.20597060311209]
  We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm's PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC's calls to an external CNF-XOR solver using proof certificates.
  arXiv  Detail & Related papers  (2024-06-17T11:02:04Z)
• Stable Nonconvex-Nonconcave Training via Linear Interpolation [51.668052890249726]
  This paper presents a theoretical analysis of linearahead as a principled method for stabilizing (large-scale) neural network training. We argue that instabilities in the optimization process are often caused by the nonmonotonicity of the loss landscape and show how linear can help by leveraging the theory of nonexpansive operators.
  arXiv  Detail & Related papers  (2023-10-20T12:45:12Z)
• 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)
• Accelerated Cyclic Coordinate Dual Averaging with Extrapolation for Composite Convex Optimization [20.11028799145883]
  We propose an Accelerated Cyclic Coordinate Dual Averaging with Extrapolation (A-CODER) method for composite convex optimization. We show that A-CODER attains the optimal convergence rate with improved dependence on the number of blocks compared to prior work. For the setting where the smooth component of the objective function is expressible in a finite sum form, we introduce a variance-reduced variant of A-CODER, VR-A-CODER, with state-of-the-art complexity guarantees.
  arXiv  Detail & Related papers  (2023-03-28T19:46:30Z)
• Understanding and Constructing Latent Modality Structures in Multi-modal Representation Learning [53.68371566336254]
  We argue that the key to better performance lies in meaningful latent modality structures instead of perfect modality alignment. Specifically, we design 1) a deep feature separation loss for intra-modality regularization; 2) a Brownian-bridge loss for inter-modality regularization; and 3) a geometric consistency loss for both intra- and inter-modality regularization.
  arXiv  Detail & Related papers  (2023-03-10T14:38:49Z)
• Linearization Algorithms for Fully Composite Optimization [61.20539085730636]
  This paper studies first-order algorithms for solving fully composite optimization problems convex compact sets. We leverage the structure of the objective by handling differentiable and non-differentiable separately, linearizing only the smooth parts.
  arXiv  Detail & Related papers  (2023-02-24T18:41:48Z)
• Mutual Exclusivity Training and Primitive Augmentation to Induce Compositionality [84.94877848357896]
  Recent datasets expose the lack of the systematic generalization ability in standard sequence-to-sequence models. We analyze this behavior of seq2seq models and identify two contributing factors: a lack of mutual exclusivity bias and the tendency to memorize whole examples. We show substantial empirical improvements using standard sequence-to-sequence models on two widely-used compositionality datasets.
  arXiv  Detail & Related papers  (2022-11-28T17:36:41Z)
• Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving [0.0]
  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.
  arXiv  Detail & Related papers  (2022-09-26T11:23:17Z)
• GroupifyVAE: from Group-based Definition to VAE-based Unsupervised Representation Disentanglement [91.9003001845855]
  VAE-based unsupervised disentanglement can not be achieved without introducing other inductive bias. We address VAE-based unsupervised disentanglement by leveraging the constraints derived from the Group Theory based definition as the non-probabilistic inductive bias. We train 1800 models covering the most prominent VAE-based models on five datasets to verify the effectiveness of our method.
  arXiv  Detail & Related papers  (2021-02-20T09:49:51Z)
• Partial Orders, Residuation, and First-Order Linear Logic [0.20305676256390934]
  We will show that adding partial order constraints in such a way as each sequent defines a unique linear order on the antecedent formulas of a sequent allows us to define many useful logical operators.
  arXiv  Detail & Related papers  (2020-08-14T13:06: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.