scholarly journals AC Simplifications and Closure Redundancies in the Superposition Calculus

2021 ◽  
pp. 200-217
Author(s):  
André Duarte ◽  
Konstantin Korovin
Keyword(s):  
Superposition Calculus

scholarly journals Model Completeness, Uniform Interpolants and Superposition Calculus

2021 ◽  
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Automated Reasoning ◽  
Quantifier Elimination ◽  
Effective Solution ◽  
Model Completeness ◽  
Present Contribution ◽  
First Order ◽  
Reduction Strategies ◽  
Infinite State Systems ◽  
Infinite State ◽  
Superposition Calculus

AbstractUniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.

scholarly journals Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs

10.29007/pmmz ◽  
2018 ◽  
Author(s):  
Sylvia Grewe ◽  
André Pacak ◽  
Mira Mezini
Keyword(s):  
Type System ◽  
Type Systems ◽  
First Order ◽  
Domain Specific ◽  
The Past ◽  
Finite Term ◽  
The Individual ◽  
Input Format ◽  
Ongoing Project ◽  
Superposition Calculus

In our ongoing project VeriTaS, we aim at automating soundness proofs for type sys- tems of domain-specific languages. In the past, we successfully used previous Vampire versions for automatically discharging many intermediate proof obligations arising within standard soundness proofs for small type systems. With older Vampire versions, encoding the individual proof problems required manual encoding of algebraic datatypes via the theory of finite term algebras. One of the new Vampire versions now supports the direct specification of algebraic datatypes and integrates reasoning about term algebras into the internally used superposition calculus.In this work, we investigate how many proof problems that typically arise within type soundness proofs different Vampire 4.1 versions can prove. Our test set consists of proof problems from a progress proof of a type system for a subset of SQL. We compare running Vampire 4.1 with our own encodings of algebraic datatypes (in untyped as well as in typed first-order logic) to running Vampire 4.1 with support for algebraic datatypes, which uses SMTLIB as input format. We observe that with our own encodings, Vampire 4.1 still proves more of our input problems. We discuss the differences between our own encoding of algebraic datatypes and the ones used within Vampire 4.1 with support for algebraic datatypes.

A Complete Superposition Calculus for Primal Grammars

2014 ◽  
Vol 53 (4) ◽  
pp. 317-350
Author(s):  
Hicham Bensaid ◽  
Nicolas Peltier
Keyword(s):  
Superposition Calculus

scholarly journals Hierarchic Superposition Revisited

10.29007/w9vg ◽  
2018 ◽  
Author(s):  
Uwe Waldmann
Keyword(s):  
Black Box ◽  
Background Model ◽  
Linear Arithmetic ◽  
Completeness Result ◽  
Standard Models ◽  
Theory Reasoning ◽  
Rational Arithmetic ◽  
Background Models ◽  
Superposition Calculus

In 1994,Bachmair, Ganzinger, and Waldmann introduced the hierarchicalsuperposition calculus as a generalization of the superpositioncalculus for black-box style theory reasoning.Their calculus works in a framework of hierarchic specifications.It tries to prove theunsatisfiability of a set of clauses with respect to interpretationsthat extend a background model such as the integers with linear arithmeticconservatively, that is, withoutidentifying distinct elements of old sorts ("confusion") and withoutadding new elements to old sorts ("junk").We show how the calculus can be improved,report on practical experiments,and present a new completeness result fornon-compact classes of background models(i.e., linear integer or rational arithmetic restricted tostandard models).

scholarly journals An Inference Rule for the Acyclicity Property of Term Algebras

10.29007/tlw4 ◽  
2018 ◽  
Author(s):  
Simon Robillard
Keyword(s):  
Computer Science ◽  
Inference Rule ◽  
Theorem Prover ◽  
Science Reasoning ◽  
First Order ◽  
Theorem Provers ◽  
Smt Solvers ◽  
Indexing Technique ◽  
Superposition Calculus

Term algebras are important structures in many areas of mathematics and computer science. Reasoning about their theories in superposition-based first-order theorem provers is made difficult by the acyclicity property of terms, which is not finitely axiomatizable. We present an inference rule that extends the superposition calculus and allows reasoning about term algebras without axioms to describe the acyclicity property. We detail an indexing technique to efficiently apply this rule in problems containing a large number of clauses. Finally we experimentally evaluate an implementation of this extended calculus in the first-order theorem prover Vampire. The results show that this technique is able to find proofs for difficult problems that existing SMT solvers and first-order theorem provers are unable to solve.

scholarly journals Satisfiability Checking and Query Answering for Large Ontologies

10.29007/n1sv ◽  
2018 ◽  
Author(s):  
Christoph Weidenbach ◽  
Patrick Wischnewski
Keyword(s):  
State Of The Art ◽  
The State ◽  
Order Logic ◽  
Query Answering ◽  
First Order Logic ◽  
First Order ◽  
Satisfiability Checking ◽  
Superposition Calculus

In this paper we develop a sound, complete and terminating superposition calculusplus a query answering calculus for the BSH-Y2 fragment of theBernays-Schoenfinkel Horn class of first-order logic.BSH-Y2 can be used to represent expressive ontologies.In addition to checking consistency, our calculus supports query answeringfor queries with arbitrary quantifier alternations.Experiments on BSH-Y2 (fragments) of several large ontologies show that ourapproach advances the state of the art.

scholarly journals Prime Implicate Generation in Equational Logic (extended abstract)

2018 ◽  
Author(s):  
Mnacho Echenim ◽  
Nicolas Peltier ◽  
Sophie Tourret
Keyword(s):  
State Of The Art ◽  
Experimental Results ◽  
Equational Logic ◽  
First Order ◽  
On Demand ◽  
Proof Search ◽  
Superposition Calculus

A procedure is proposed to efficiently generate sets of ground implicates of first-order formulas with equality. It is based on a tuning of the superposition calculus, enriched with rules that add new hypotheses on demand during the proof search. Experimental results are presented, showing that the proposed approach is more efficient than state-of-the-art systems.

scholarly journals Superposition with Lambdas

2021 ◽  
Author(s):  
Alexander Bentkamp ◽  
Jasmin Blanchette ◽  
Sophie Tourret ◽  
Petar Vukmirović ◽  
Uwe Waldmann
Keyword(s):  
Higher Order ◽  
Equivalence Classes ◽  
Order Logic ◽  
Inference Rules ◽  
Higher Order Logic ◽  
Superposition Calculus

AbstractWe 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 $$\lambda $$ λ -terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.

scholarly journals Separation logic + superposition calculus = heap theorem prover

2011 ◽  
Vol 46 (6) ◽  
pp. 556-566 ◽  
Author(s):  
Juan Antonio Navarro Pérez ◽  
Andrey Rybalchenko
Keyword(s):  
Separation Logic ◽  
Theorem Prover ◽  
Superposition Calculus
Sign in / Sign up

Export Citation Format

Share Document