Related papers: Optimistic Higher-Order Superposition

Optimistic Higher-Order Superposition

URL: http://arxiv.org/abs/2510.18429v1
Date: Tue, 21 Oct 2025 09:05:54 GMT
Title: Optimistic Higher-Order Superposition
Authors: Alexander Bentkamp, Jasmin Blanchette, Matthias Hetzenberger, Uwe Waldmann,
Abstract summary: We introduce an "optimistic" version of the $lambda$-superposition calculus.<n>It delays explosive unification problems using constraints stored along with the clauses, and it applies functional extensionality in a more targeted way.<n>We have yet to implement it in a prover, but examples suggest that it will outperform, or at least usefully complement, the original calculus.
Score: 39.146761527401424
License: http://creativecommons.org/licenses/by/4.0/
Abstract: The $\lambda$-superposition calculus is a successful approach to proving higher-order formulas. However, some parts of the calculus are extremely explosive, notably due to the higher-order unifier enumeration and the functional extensionality axiom. In the present work, we introduce an "optimistic" version of $\lambda$-superposition that addresses these two issues. Specifically, our new calculus delays explosive unification problems using constraints stored along with the clauses, and it applies functional extensionality in a more targeted way. The calculus is sound and refutationally complete with respect to a Henkin semantics. We have yet to implement it in a prover, but examples suggest that it will outperform, or at least usefully complement, the original $\lambda$-superposition calculus.

Related papers

Constructive Approximation under Carleman's Condition, with Applications to Smoothed Analysis [13.02728413691724]
We develop a fairly tight analogue of the underlying DenjoyCarleman via complex analysis.<n>We establish $L2$ approximation-theoretic results for functions over general classes of distributions.<n>As another application, we show that the Paley--Wiener class of functions band to $[-,]$ admits superexponential rates of approximation over all strictly sub-exponential distributions.
arXiv Detail & Related papers (2025-12-04T01:40:05Z)
Non-Euclidean High-Order Smooth Convex Optimization [9.940728137241214]
We develop algorithms for the optimization of convex objectives that have H"older continuous $q$-th derivatives.<n>Our algorithms work for general norms under mild conditions, including the $ell_p$-settings for $1leq pleq infty$.
arXiv Detail & Related papers (2024-11-13T19:22:34Z)
Tempered Calculus for ML: Application to Hyperbolic Model Embedding [70.61101116794549]
Most mathematical distortions used in ML are fundamentally integral in nature. In this paper, we unveil a grounded theory and tools which can help improve these distortions to better cope with ML requirements. We show how to apply it to a problem that has recently gained traction in ML: hyperbolic embeddings with a "cheap" and accurate encoding along the hyperbolic vsean scale.
arXiv Detail & Related papers (2024-02-06T17:21:06Z)
First and zeroth-order implementations of the regularized Newton method with lazy approximated Hessians [4.62316736194615]
We develop Lip-order (Hessian-O) and zero-order (derivative-free) implementations of general non-free$ normfree problems. We also equip our algorithms with the lazy bound update that reuses a previously computed Hessian approximation matrix for several iterations.
arXiv Detail & Related papers (2023-09-05T17:40:54Z)
Lower Bounds and Accelerated Algorithms for Bilevel Optimization [62.192297758346484]
Bilevel optimization has recently attracted growing interests due to its wide applications in modern machine learning problems. We show that our results are more challenging than that of minimax applications.
arXiv Detail & Related papers (2021-02-07T21:46:29Z)
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)
High-Order Oracle Complexity of Smooth and Strongly Convex Optimization [31.714928102950584]
We consider the complexity of optimizing a highly smooth (Lipschitz $k$-th order derivative) and strongly convex function, via calls to a $k$-th order oracle. We prove that the worst-case oracle complexity for any fixed $k$ to optimize the function up to accuracy $epsilon$ is on the order of $left.
arXiv Detail & Related papers (2020-10-13T19:18:15Z)
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.