Related papers: On the Proof Complexity of Deep Inference
We study the derivational complexity of rewrite systems whose termination is provable in the dependency pair framework using the processors for reduction pairs, dependency graphs, or the subterm criterion. We show that the derivational…
In this short note we give an alternative proof of Glivenko's Theorem, stating that a formula $\phi$ is provable in classical propositional logic if and only if $\neg\neg\phi$ is provable in intuitionistic propositional logic. We work in…
The unified correspondence theory for distributive lattice expansion logics (DLE-logics) is specialized to strict implication logics. As a consequence of a general semantic consevativity result, a wide range of strict implication logics can…
This paper studies the form and complexity of inference in graphical models using the abstraction offered by algebraic structures. In particular, we broadly formalize inference problems in graphical models by viewing them as a sequence of…
Credal networks are graph-based statistical models whose parameters take values in a set, instead of being sharply specified as in traditional statistical models (e.g., Bayesian networks). The computational complexity of inferences on such…
By affine arithmetic is meant the set of affine consequences of Peano arithmetic. This is a continuous theory which is studied in the framework of affine logic, a sublogic of continuous logic. Affine arithmetic is undecidable. Also, its…
In this paper, we demonstrate how to do automated theorem proving in the presence of a large knowledge base of potential premises without learning from human proofs. We suggest an exploration mechanism that mixes in additional premises…
We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus,…
This article presents a technique for proving problems hard for classes of the polynomial hierarchy or for PSPACE. The rationale of this technique is that some problem restrictions are able to simulate existential or universal quantifiers.…
We introduce the Delta-framework, LF-Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union.…
This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these…
It is an original method based on systems of prameters represented by reals which obey to an infinite descent (convergent sequences). We define calculus of quotients and they conduct quickly to a consequent result. Our own scepticism made…
We present a method to prove the decidability of provability in several well-known inference systems. This method generalizes both cut-elimination and the construction of an automaton recognizing the provable propositions.
This article describes the *Confluence Framework*, a novel framework for proving and disproving confluence using a divide-and-conquer modular strategy, and its implementation in CONFident. Using this approach, we are able to automatically…
Italian master's thesis in Computer Science. It is an overview of the standard tecniques developed in the field of Proof Theory, ending with some results in the new field of Deep Inference, plus an original contribution trying to relate…
This note is about the relationship between two theories of negation as failure -- one based on program completion, the other based on stable models, or answer sets. Francois Fages showed that if a logic program satisfies a certain…
We give a general reduction of lengths-of-proofs lower bounds for constant depth Frege systems in DeMorgan language augmented by a connective counting modulo a prime $p$ (the so called $AC^0[p]$ Frege systems) to computational complexity…
We examine the meaning and the complexity of probabilistic logic programs that consist of a set of rules and a set of independent probabilistic facts (that is, programs based on Sato's distribution semantics). We focus on two semantics,…
In this extended abstract, we discuss the opportunity to formally verify that inference systems for probabilistic programming guarantee good performance. In particular, we focus on hybrid inference systems that combine exact and approximate…
We prove that the problem of determining whether a finite logical matrix determines an algebraizable logic is complete for EXPTIME. The same result holds for the classes of order algebraizable, weakly algebraizable, equivalential and…