scholarly journals First-Order Interpolation and Interpolating Proof Systems

10.29007/1qb8 ◽  
2018 ◽  
Author(s):  
Laura Kovács ◽  
Andrei Voronkov
Keyword(s):  
Proof System ◽  
First Order ◽  
Proof Systems ◽  
Quantifier Complexity ◽  
Non Local ◽  
Additional Constraints ◽  
Superposition Calculus

It is known that one can extract Craig interpolants from so-called localproofs. An interpolant extracted from such a proof is a booleancombination of formulas occurring in the proof. However, standard completeproof systems, such as superposition, for theories having the interpolationproperty are not necessarily complete for local proofs: there are formulashaving non-local proofs but no local proof.In this paper we investigate interpolant extraction from non-local refutations(proofs of contradiction) in the superposition calculus and prove a numberof general results about interpolant extraction and complexity of extractedinterpolants. In particular, we prove that the number of quantifier alternationsin first-order interpolants of formulas without quantifier alternations isunbounded. This result has far-reaching consequences for using local proofsas a foundation for interpolating proof systems: any such proof system shoulddeal with formulas of arbitrary quantifier complexity.To search for alternatives for interpolating proof systems, we consider severalvariations on interpolation and local proofs. Namely, we give an algorithm forbuilding interpolants from resolution refutations in logic without equality anddiscuss additional constraints when this approach can be also used for logicwith equality. We finally propose a new direction related to interpolation vialocal proofs in first-order theories.

scholarly journals A duality between proof systems for cyclic term graphs

2007 ◽  
Vol 17 (3) ◽  
pp. 439-484 ◽  
Author(s):  
CLEMENS GRABMAYER
Keyword(s):  
Close Connection ◽  
Proof System ◽  
Consistency Checking ◽  
Duality Result ◽  
First Order ◽  
Proof Systems ◽  
Similar Proof ◽  
Equational Specifications ◽  
Cyclic Term

This paper presents a proof-theoretic observation about two kinds of proof systems for bisimilarity between cyclic term graphs.First we consider proof systems for demonstrating that μ term specifications of cyclic term graphs have the same tree unwinding. We establish a close connection between adaptations for μ terms over a general first-order signature of the coinductive axiomatisation of recursive type equivalence by Brandt and Henglein (Brandt and Henglein 1998) and of a proof system by Ariola and Klop (Ariola and Klop 1995) for consistency checking. We show that there exists a simple duality by mirroring between derivations in the former system and formalised consistency checks, which are called ‘consistency unfoldings', in the latter. This result sheds additional light on the axiomatisation of Brandt and Henglein: it provides an alternative soundness proof for the adaptation considered here.We then outline an analogous duality result that holds for a pair of similar proof systems for proving that equational specifications of cyclic term graphs are bisimilar.

scholarly journals Reasoning Inside The Box: Deduction in Herbrand Logics

10.29007/kx2m ◽  
2018 ◽  
Author(s):  
Liron Cohen ◽  
Yoni Zohar
Keyword(s):  
Automated Reasoning ◽  
Proof System ◽  
First Order ◽  
Proof Systems ◽  
The Rich ◽  
Order Structures ◽  
Effective Proof

Herbrand structures are a subclass of standard first-order structures commonly used in logic and automated reasoning due to their strong definitional character. This paper is devoted to the logics induced by them: Herbrand and semi-Herbrand logics, with and without equality. The rich expressiveness of these logics entails that there is no adequate effective proof system for them. We therefore introduce infinitary proof systems for Herbrand logics, and prove their completeness. Natural and sound finitary approximations of the infinitary systems are also presented.

scholarly journals Constructing weak simulations from linear implications for processes with private names

2019 ◽  
Vol 29 (8) ◽  
pp. 1275-1308 ◽  
Author(s):  
Ross Horne ◽  
Alwen Tiu
Keyword(s):  
Expressive Power ◽  
Dual Pair ◽  
Proof System ◽  
Branching Time ◽  
First Order ◽  
Order Extension

AbstractThis paper clarifies that linear implication defines a branching-time preorder, preserved in all contexts, when used to compare embeddings of process in non-commutative logic. The logic considered is a first-order extension of the proof system BV featuring a de Morgan dual pair of nominal quantifiers, called BV1. An embedding of π-calculus processes as formulae in BV1 is defined, and the soundness of linear implication in BV1 with respect to a notion of weak simulation in the π -calculus is established. A novel contribution of this work is that we generalise the notion of a ‘left proof’ to a class of formulae sufficiently large to compare embeddings of processes, from which simulating execution steps are extracted. We illustrate the expressive power of BV1 by demonstrating that results extend to the internal π -calculus, where privacy of inputs is guaranteed. We also remark that linear implication is strictly finer than any interleaving preorder.

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 Monogamy of non-local quantum correlations

2008 ◽  
Vol 465 (2101) ◽  
pp. 59-69 ◽  
Author(s):  
Ben Toner
Keyword(s):  
Probability Distributions ◽  
Bell Inequality ◽  
Arbitrary Dimension ◽  
Bell Inequalities ◽  
Quantum Correlations ◽  
Interactive Proof ◽  
Proof Systems ◽  
Non Local ◽  
A New Technique ◽  
Tsirelson Bound

We describe a new technique for obtaining Tsirelson bounds, which are upper bounds on the quantum value of a Bell inequality. Since quantum correlations do not allow signalling, we obtain a Tsirelson bound by maximizing over all no-signalling probability distributions. This maximization can be cast as a linear programme. In a setting where three parties, A, B and C, share an entangled quantum state of arbitrary dimension, we (i) bound the trade-off between AB's and AC's violation of the Clauser–Horne–Shimony–Holt inequality and (ii) demonstrate that forcing B and C to be classically correlated prevents A and B from violating certain Bell inequalities, relevant for interactive proof systems and cryptography.

scholarly journals VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC

2002 ◽  
Vol 13 (03) ◽  
pp. 315-340 ◽  
Author(s):  
J. I. DEN HARTOG ◽  
E. P. DE VINK
Keyword(s):  
Programming Language ◽  
Denotational Semantics ◽  
Order Logic ◽  
First Order Logic ◽  
Proof System ◽  
Probabilistic Choice ◽  
First Order ◽  
Probabilistic Programs

Probability, be it inherent or explicitly introduced, has become an important issue in the verification of programs. In this paper we study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs, a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify propertics of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates is introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to be sound and complete; the properties that can be derived are exactly the valid properties. Finally some typical examples illustrate the use of the probabilistic predicates and the proof system.

A Non-Local Convective Flux Limiter for Upwind-Biased Finite Volume Simulations

2010 ◽  
Author(s):  
Nicole M. W. Poe ◽  
D. Keith Walters
Keyword(s):  
Finite Volume ◽  
Finite Volume Methods ◽  
Second Order ◽  
Numerical Dissipation ◽  
Ansys Fluent ◽  
First Order ◽  
Low Dissipation ◽  
Solution Convergence ◽  
Improve Accuracy ◽  
Non Local

Finite volume methods on structured and unstructured meshes often utilize second-order, upwind-biased linear reconstruction schemes to approximate the convective terms, in an attempt to improve accuracy over first-order methods. Limiters are employed to reduce the inherent variable over- and under-shoot of these schemes; however, they also can significantly increase the numerical dissipation of a solution. This paper presents a novel non-local, non-monotonic (NLNM) limiter developed by enforcing cell minima and maxima on dependent variable values projected to cell faces. The minimum and maximum values for a cell are determined primarily through the recursive reference to the minimum and maximum values of its upwind neighbors. The new limiter is implemented using the User Defined Function capability available in the commercial CFD solver Ansys FLUENT. Various simple test cases are presented which exhibit the NLNM limiter’s ability to eliminate non-physical oscillations while maintaining relatively low dissipation of the solution. Results from the new limiter are compared with those from other limited and unlimited second-order upwind (SOU) and first-order upwind (FOU) schemes. For the cases examined in the study, the NLNM limiter was found to improve accuracy without significantly increasing solution convergence rate.

Sign in / Sign up

Export Citation Format

Share Document