Related papers: Superposition for Lambda-Free Higher-Order Logic
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…
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…
We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern cannot, in general, be described by a pattern, or even by a…
We generalize several propositional preprocessing techniques to higher-order logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of…
Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably…
Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the…
We prove a topological completeness theorem for the modal logic GLP containing operators $\langle\lambda\rangle$ for $\lambda \in$ Ord intended to capture progressively stronger notions of consistency in mathematical theories. We show that,…
Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the…
In functional programming, point-free relation calculi have been fruitful for general theories of program construction, but for specific applications pointwise expressions can be more convenient and comprehensible. In imperative…
Hybrid logic extends modal logic with special propositions called nominals, each of which is true at only one state in a model. This enables us to describe some properties of binary relations, such as irreflexivity and anti-symmetry, which…
Modern saturation-based Automated Theorem Provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implementations of this calculus use a variety of literal selections…
In this work we provide alternative formulations of the concepts of lambda theory and extensional theory without introducing the notion of substitution and the sets of all, free and bound variables occurring in a term. We also clarify the…
A sound and complete embedding of conditional logics into classical higher-order logic is presented. This embedding enables the application of off-the-shelf higher-order automated theorem provers and model finders for reasoning within and…
For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on $\mathbb{N}^d$ (Dickson's lemma), yielding Ackermannian upper bounds via controlled bad-sequence…
The typical mathematical language systematically exploits notational and logical abuses whose resolution requires not just the knowledge of domain specific notation and conventions, but not trivial skills in the given mathematical…
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. The completeness…
Refutation calculi are formal systems developed to derive the invalid formulas of a given logic. While the notion of refutation calculi has played a key role in the development of tableaux calculi, a refutation approach to display calculi…
In this paper we present two terminating tableau calculi for propositional Dummett logic obeying the subformula property. The ideas of our calculi rely on the linearly ordered Kripke semantics of Dummett logic. The first calculus works on…
We introduce $\lambda$KBO and $\lambda$LPO, two variants of the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) designed for use with the $\lambda$-superposition calculus. We establish the desired properties via encodings…
We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut-elimination and subformula property. Based on the same design,…