VSE knjižnice (vzajemna bibliografsko-kataložna baza podatkov COBIB.SI)
-
Sequent calculi for induction and infinite descentBrotherston, James ; Simpson, AlexThis article formalizes and compares two different styles of reasoning with inductively defined predicates, each style being encapsulated by a corresponding sequent calculus proof system. The first ... system, LKID, supports traditional proof by induction, with induction rules formulated as rules for introducing inductively defined predicates on the left of sequents. We show LKID to be cut-free complete with respect to a natural class of Henkin models; the eliminability of cut follows as a corollary. The second system, ▫$\text{LKID}^\omega$▫, uses infinite (non-well-founded) proofs to represent arguments by infinite descent. In this system, the left-introduction rules for inductively defined predicates are simple case-split rules, and an infinitary, global condition on proof trees is required in order to ensure soundness. We show ▫$\text{LKID}^\omega$▫ to be cut-free complete with respect to standard models, and again infer the eliminability of cut. The infinitary system ▫$\text{LKID}^\omega$▫ is unsuitable for formal reasoning. However, it has a natural restriction to proofs given by regular trees, i.e. to those proofs representable by finite graphs, which is so suited. We demonstrate that this restricted "cyclic" proof system, ▫$\text{CLKID}^\omega$▫, subsumes LKID, and conjecture that ▫$\text{CLKID}^\omega$▫ and LKID are in fact equivalent, i.e. that proof by induction is equivalent to regular proof by infinite descent.ard effect calculi (such as those based on monads), and to models of intuitionistic linear logic. We also prove soundness and completeness.Vir: Journal of logic and computation. - ISSN 0955-792X (Vol. 21, no. 6, 2011, str. 1177-1216)Vrsta gradiva - članek, sestavni delLeto - 2011Jezik - angleškiCOBISS.SI-ID - 17091929
Vnos na polico
Trajna povezava
- URL:
Faktor vpliva
Dostop do baze podatkov JCR je dovoljen samo uporabnikom iz Slovenije. Vaš trenutni IP-naslov ni na seznamu dovoljenih za dostop, zato je potrebna avtentikacija z ustreznim računom AAI.
Leto | Faktor vpliva | Izdaja | Kategorija | Razvrstitev | ||||
---|---|---|---|---|---|---|---|---|
JCR | SNIP | JCR | SNIP | JCR | SNIP | JCR | SNIP |
Baze podatkov, v katerih je revija indeksirana
Ime baze podatkov | Področje | Leto |
---|
Povezave do osebnih bibliografij avtorjev | Povezave do podatkov o raziskovalcih v sistemu SICRIS |
---|---|
Brotherston, James | |
Simpson, Alex | 37834 |
Vir: Osebne bibliografije
in: SICRIS
Izberite prevzemno mesto:
Prevzem gradiva po pošti
Naslov za dostavo:
Med podatki člana manjka naslov.
Storitev za pridobivanje naslova trenutno ni dostopna, prosimo, poskusite še enkrat.
S klikom na gumb "V redu" boste potrdili zgoraj izbrano prevzemno mesto in dokončali postopek rezervacije.
S klikom na gumb "V redu" boste potrdili zgoraj izbrano prevzemno mesto in naslov za dostavo ter dokončali postopek rezervacije.
S klikom na gumb "V redu" boste potrdili zgoraj izbrani naslov za dostavo in dokončali postopek rezervacije.
Obvestilo
Trenutno je storitev za avtomatsko prijavo in rezervacijo nedostopna. Gradivo lahko rezervirate sami na portalu Biblos ali ponovno poskusite tukaj kasneje.
Gesla v Splošnem geslovniku COBISS
Izbira mesta prevzema
Gradivo iz matične enote je brezplačno. Če je gradivo na mesto prevzema dostavljeno iz drugih enot, lahko knjižnica to storitev zaračuna.
Mesto prevzema | Status gradiva | Rezervacija |
---|
Rezervacija v teku
Prosimo, počakajte trenutek.
Rezervacija je uspela.
Rezervacija ni uspela.
Rezervacija...
Članska izkaznica:
Mesto prevzema: