Wyniki wyszukiwania - BazTech

Ograniczanie wyników

4 Fundamenta Informaticae

Powiadomienia systemowe

Sesja wygasła!
Sesja wygasła!

Znaleziono wyników: 4

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: cut elimination

Sortuj według:

Ogranicz wyniki do:

Intersection Types with Subtyping by Means of Cut Elimination

Laurent O.

Fundamenta Informaticae

2012

Vol. 121, nr 1/4

203-226

We give a purely syntactic proof (from scratch) of the subject equality property of the BCD intersection type system through a reformulation of the subtyping relation having a "cut- elimination" property.

Foundations of Paraconsistent Resolution

Kamide N.

Fundamenta Informaticae

2006

Vol. 71, nr 4

419-441

An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness theorem (with respect to a classical-like semantics) and cut-elimination theorem are proved for PLK. The correspondence between PLK and PRC is shown by using a faithful embedding of PLK into the sequent calculus LK for classical logic.

Strong normalisation of cut-elimination in clasical logic

Urban C., Bierman G.M.

Fundamenta Informaticae

2001

Vol. 45, nr 1,2

123-155

In this paper we present a strongly normalising cut-elimination procedure for classical logic. This procedure adapts Gentzen's standard cut-reductions, but is less restrictive than previous strongly normalising cut-elimination procedures. In comparison, for example, with works by Dragalin and Danos et al., our procedure requires no special annotations on formulae and allows cut-rules to pass over other cut-rules. In order to adapt the notion of symmetric reducibility candidates for proving the strong normalisation property, we introduce a novel term assignment for sequent proofs of classical logic and formalise cut-reductions as term rewriting rules.

Multi lingual sequent calculus and coherent spaces

Jung A., Kegelmann M.

Fundamenta Informaticae

1999

Vol. 37, Nr 4

369-412

We study a Gentzen style sequent calculus where the formulas on the left and right of the turnstile need not necessarily come from the same logical system. Such a sequent can be seen as a consequence between different domains of reasoning. We discuss the ingredients needed to set up the logic generalized in this fashion. The usual cut rule does not make sense for sequents which connect different logical systems because it mixes formulas from antecedent and succedent. We propose a different cut rule which addresses this problem. The new cut rule can be used as a basis for composition in a suitable category of logical sys-tems. As it turns out, this category is equivalent to coherent spaces with certain relations be-tween them. Finally, cut elimination in this set-up can be employed to provide a new explanation of the domain constructions in Samson Abramsky's Domain Theory in Logical Form.