PL
 |
EN
Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 13

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  proof theory
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Reverse mathematics of some topics from algorithmic graph theory
100%
Clote P. G. , Hirst J. L.
Fundamenta Mathematicae
|
1998
|
tom 157
|
nr 1
1-13
EN
This paper analyzes the proof-theoretic strength of an infinite version of several theorems from algorithmic graph theory. In particular, theorems on reachability matrices, shortest path matrices, topological sorting, and minimal spanning trees are considered.
2
Hypersequent Calculi for S5: The Methods of Cut Elimination
100%
Bednarska K. , Indrzejczak A.
Logic and Logical Philosophy
|
2015
|
tom 24
|
nr 3
277–311
EN
S5 is one of the most important modal logic with nice syntactic, semantic and algebraic properties. In spite of that, a successful (i.e. cut-free) formalization of S5 on the ground of standard sequent calculus (SC) was problematic and led to the invention of numerous nonstandard, generalized forms of SC. One of the most interesting framework which was very often used for this aim is that of hypersequent calculi (HC). The paper is a survey of HC for S5 proposed by Pottinger, Avron, Restall, Poggiolesi, Lahav and Kurokawa. We are particularly interested in examining different methods which were used for proving the eliminability/admissibility of cut in these systems and present our own variant of a system which admits relatively simple proof of cut elimination.
3
Content available remote A Semantic Analysis of a Logic for Pragmatics with Assertions, Obligations, and Causal Implication
100%
Ranalter K.
Fundamenta Informaticae
|
2008
|
tom Vol. 84, nr 3-4
443-470
EN
One of the aims of a logic for pragmatics is to provide a logical framework that formalizes reasoning about speech acts. In this paper we investigate the semantics of a fragment of the logic for pragmatics proposed by Bellin and Dalla Pozza in "A pragmatic interpretation of substructural logics" (Feferman Festschrift, ASL Lecture Notes in Logic 15, 2002). The logic deals with acts of assertion and acts of obligation, and it incorporates a rule that relates acts of obligation to acts of assertion via a notion of causal implication. As our main result we show that the logic is sound and complete with respect to a class of algebraic, Kripke, and categorical models.
4
Content available Rule-Generation Theorem and its Applications
100%
Indrzejczak A.
Bulletin of the Section of Logic
|
2018
|
tom 47
|
nr 4
EN
In several applications of sequent calculi going beyond pure logic, an introduction of suitably defined rules seems to be more profitable than addition of extra axiomatic sequents. A program of formalization of mathematical theories via rules of special sort was developed successfully by Negri and von Plato. In this paper a general theorem on possible ways of transforming axiomatic sequents into rules in sequent calculi is proved. We discuss its possible applications and provide some case studies for illustration.
5
Content available remote Skolem’s Theorem in Coherent Logic
100%
Bezem M. , Coquand T.
Fundamenta Informaticae
|
2019
|
tom Vol. 170, nr 1-3
1--14
EN
We give a constructive proof of Skolem's Theorem for coherent logic and discuss several applications, including a negative answer to a question by Wraith.
6
Content available A proof-theoretic approach to scope ambiguity in compositional vector space models
100%
Wijnholds G. J.
Journal of Language Modelling
|
2018
|
tom Vol. 6, No. 2
261--286
EN
We investigate the extent to which compositional vector space models can be used to account for scope ambiguity in quantified sentences (of the form Every man loves some woman). Such sentences containing two quantifiers introduce two readings, a direct scope reading and an inverse scope reading. This ambiguity has been treated in a vector space model using bialgebras by Hedges and Sadrzadeh (2016) and Sadrzadeh (2016), though without an explanation of the mechanism by which the ambiguity arises. We combine a polarised focussed sequent calculus for the non-associative Lambek calculus NL, as described in Moortgat and Moot (2011), with the vector-based approach to quantifier scope ambiguity. In particular, we establish a procedure for obtaining a vector space model for quantifier scope ambiguity in a derivational way.
7
Sequents for non-wellfounded mereology
100%
Maffezioli P.
Logic and Logical Philosophy
|
2016
|
tom 25
|
nr 3 Mereology and Beyond (II)
351-369
EN
The paper explores the proof theory of non-wellfounded mereology with binary fusions and provides a cut-free sequent calculus equivalent to the standard axiomatic system.
8
Content available remote Investigating the Logical Aspects of the Pi-calculus
88%
Bernard N.
Schedae Informaticae
|
2003
|
tom Vol. 12
57-66
EN
The relations between the p-calculus and logic have been less extensively studied than for the l-calculus. We give an account on what can be found in the literature, in two distinct directions: model-checking, and typing. We propose a Curry-Howard correspondence taking into account the dynamic properties of the p-calculus. This is a first presentation of a work in progress.
9
Content available remote Proof-graphs: a Thorough Cycle Treatment, Normalization and Subformula Property
88%
Alve G. V. , Oliveira A. G. d. , Queiroz R. d.
Fundamenta Informaticae
|
2011
|
tom Vol. 106, nr 2-4
119-147
EN
A normalization procedure is presented for a classical natural deduction (ND) proof system. This proof system, called N-Graphs, has a multiple conclusion proof structure, where cycles are allowed. With this, we have developed a thorough treatment of cycles, including cycles normalization via an algorithm. We also demonstrate the usefulness of the graphical framework of N-Graphs, where derivations are seen as digraphs. We use geometric perspective techniques to establish the normalization mechanism, thus giving a direct normalization proof. Moreover, the subformula and separation properties are determined.
10
Content available remote Graphs and Colorings for Answer Set Programming with Preferences
88%
Konczak K. , Schaub T. , Linke T.
Fundamenta Informaticae
|
2003
|
tom Vol. 57, nr 2-4
393--421
EN
The integration of preferences into answer set programming constitutes an important practical device for distinguishing certain preferred answer sets from non-preferred ones. To this end, we elaborate upon rule dependency graphs and their colorings for characterizing different preference handling strategies found in the literature. We start from a characterization of (three types of) preferred answer sets in terms of totally colored dependency graphs. In particular, we demonstrate that this approach allows us to capture all three approaches to preferences in a uniform setting by means of the concept of a height function. In turn, we exemplarily develop an operational characterization of preferred answer sets in terms of operators on partial colorings for one particular strategy. In analogy to the notion of a derivation in proof theory, our operational characterization is expressed as a (non-deterministically formed) sequence of colorings, gradually turning an uncolored graph into a totally colored one.
11
Content available remote Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis
75%
Petrukhin Y. , Shangin V.
Logic and Logical Philosophy
|
2019
|
tom 28
|
nr 2
223–257
EN
Using the method of correspondence analysis, Tamminga obtains sound and complete natural deduction systems for all the unary and binary truth-functional extensions of Kleene’s strong three-valued logic K3 . In this paper, we extend Tamminga’s result by presenting an original finite, sound and complete proof-searching technique for all the truth-functional binary extensions of K3.
12
Content available A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics
63%
Gao F. , Tourlakis G.
|
|
nr 3-4
EN
A well established technique toward developing the proof theory of a Hilbert-style modal logic is to introduce a Gentzen-style equivalent (a Gentzenisation), then develop the proof theory of the latter, and finally transfer the metatheoretical results to the original logic (e.g., [1, 6, 8, 18, 10, 12]). In the first-order modal case, on one hand we know that the Gentzenisation of the straightforward first-order extension of GL, the logic QGL, admits no cut elimination (if the rule is included as primitive; or, if not included, then the rule is not admissible [1]). On the other hand the (cut-free) Gentzenisations of the first-order modal logics M3 and ML3 of [10, 12] do have cut as an admissible rule. The syntactic cut admissibility proof given in [18] for the Gentzenisation of the propositional provability logic GL is extremely complex, and it was the basis of the proofs of cut admissibility of the Gentzenisations of M3 and ML3, where the presence of quantifiers and quantifier rules added to the complexity and length of the proof. A recent proof of cut admissibility in a cut-free Gentzenisation of GL is given in [5] and is quite short and easy to read. We adapt it here to revisit the proofs for the cases of M3 and ML3, resulting to similarly short and easy to read proofs, only slightly complicated by the presence of quantification and its relevant rules.
13
Content available A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs
63%
Tourlakis G.
Bulletin of the Section of Logic
|
2016
|
tom 45
|
nr 1
EN
Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is (provably, [2]) unavailable. This paper applies the formulator approach to show the independence of the axiom schema ☐A → ☐∀ A of the logics M3and ML3 of [17, 18, 11, 13]. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations.  In particular, the so modified ML3 is, similarly to QGL, an arithmetically incomplete first-order extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics (compare with the more complexproofs in [2,8]).
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.