Superposition for Lambda-Free Higher-Order Logic
We introduce refutationally complete superposition calculi for intentional and extensional clausal $\lambda$-free higher-order logic, two formalisms that allow partial application and applied variables. 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. We implemented the calculi in the Zipperposition prover and evaluated them on Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone towards complete, highly efficient automatic theorem provers for full higher-order logic.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Superposition with Lambdas
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 class…
Abstract categorial grammars with island constraints and effective decidability
A well-known approach to treating syntactic island constraints in the setting of Lambek grammars consists in adding specific bracket modalities to the logic. We adapt this approach to abstract categorial grammars (ACG). …
Optimistic Higher-Order Superposition
The $λ$-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 functiona…
Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in …
NegationUniversal Dependencies to Logical Forms with Negation Scope
Many language technology applications would benefit from the ability to represent negation and its scope on top of widely-used linguistic resources. In this paper, we investigate the possibility of obtaining a first-orde…
Negation