CINECA IRIS Institutional Research Information System
IRIS è l'Anagrafe della ricerca dell'Università degli Studi di Trento, e ha lo scopo di raccogliere, documentare, conservare e diffondere, anche ad accesso aperto, la produzione scientifica degli autori afferenti all'Università degli Studi di Trento.
EnglishIn deep inference, in contrast to traditional proof-theoretic methodologies, inference rules can be applied at any depth inside logical expressions. This makes it possible to design deductive systems that are tailored for computer science applications and otherwise provably not expressible. With deep inference, we can simulate analytic proofs in traditional deductive formalisms, and also construct much shorter analytic proofs. However, deep applicability of inference rules causes a greater nondeterminism in proof construction. This thesis studies the problem of dealing with nondeterminism in proof search while preserving the shorter proofs. By redesigning the deductive systems, some redundant rule applications are prevented. By introducing a new technique which reduces nondeterminism, it becomes possible to obtain a more immediate access to shorter proofs without breaking proof theoretic properties such as cut-elimination. Different implementations presented allow to perform experiments and observe the performance improvements. Within a computation-as-proof-search perspective, we use these deductive systems to develop a common proof-theoretic language for planning and concurrency.
Scheda prodotto non validato
I dati visualizzati non sono stati ancora sottoposti a validazione formale da parte dello Staff di IRIS, ma sono stati ugualmente trasmessi al Sito Docente Cineca (Loginmiur).
| Titolo: | Nondeterminism and Language Design in Deep Inference: A Proof Theoretic Approach to Logic Programming |
| Autori: | Kahramanogullari, Ozan |
| Autori Unitn: | |
| Luogo di edizione: | Saarbruecken |
| Casa editrice: | LAP LAMBERT Academic Publishing |
| Anno di pubblicazione: | 2012 |
| ISBN: | 9783659134753 |
| Handle: | http://hdl.handle.net/11572/99943 |
| Appare nelle tipologie: | 01.1 Libro in qualità di autore (Book as author) |
File in questo prodotto:
Copyright © 2020