相关论文: A short proof of the Strong Normalization of Class…

We demonstrate that the classical Michael selection theorem for l.s.c. mappings with a collectionwise normal domain can be reduced only to compact-valued mappings modulo Dowker's extension theorem for such spaces. The idea used to achieve…

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.

In this paper, we use a new method to prove cut-elimination of weak intuitionistic tense logic. This method focuses on splitting the contraction rule and cut rules. Further general theories and applications of this method shall be developed…

We consider the immediate consequence of an arguable addition to the standard Deduction Theorems of first order theories.

In previous work we provided a method for eliminating cuts in non-wellfounded proofs with a local-progress condition, these being the simplest kind of non-wellfounded proofs. The method consisted of splitting the proof into nicely behaved…

We discuss proving correctness and completeness of definite clause logic programs. We propose a method for proving completeness, while for proving correctness we employ a method which should be well known but is often neglected. Also, we…

We introduce a notion of the ``explanation" of one (generalized) probabilistic model by another as particular kind of span in the category $\Prob$ of probabilistic models and morphisms. We show that explanations compose under a standard…

It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. The aim of this work is to study…

We introduce `atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flows that correspond to complex reductions on derivations.…

Conceiving of premises as collected into sets or multisets, instead of sequences, may lead to triviality for classical and intuitionistic logic in general proof theory, where we investigate identity of deductions. Any two deductions with…

The goal of this note is to compare two notions, one coming from the theory of rewrite systems and the other from proof theory: confluence and cut elimination. We show that to each rewrite system on terms, we can associate a logical system:…

Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of…

We present a general method to derive the classical mechanics of a system of identical particles in a way that retains information about quantum statistics. The resulting statistical mechanics can be interpreted as a classical version of…

In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This…

These are notes on discrete mathematics for computer scientists. The presentation is somewhat unconventional. Indeed I begin with a discussion of the basic rules of mathematical reasoning and of the notion of proof formalized in a natural…

We study the problem of probabilistic deduction with conditional constraints over basic events. We show that globally complete probabilistic deduction with conditional constraints over basic events is NP-hard. We then concentrate on the…

In this article, we define general normal forms for any logic that has propositional part and whose non-propositional connectives distribute over the finite disjunctions. We do not require the non-propositional connectives to be closed on…

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations, and explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all…

The logic of constant domains is intuitionistic logic extended with the so-called forall-shift axiom, a classically valid statement which implies the excluded middle over decidable formulas. Surprisingly, this logic is constructive and so…

We give labeled natural deduction systems for a family of tense logics extending the basic linear tense logic Kl. We prove that our systems are sound and complete with respect to the usual Kripke semantics, and that they possess a number of…