Cantitate/Preț
Produs

Nondeterminism and Language Design in Deep Inference

Autor Ozan Kahramanoğulları
en Limba Engleză Paperback – 2 iul 2012
In 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.
Citește tot Restrânge

Preț: 44778 lei

Preț vechi: 55973 lei
-20% Nou

Puncte Express: 672

Preț estimativ în valută:
8569 8892$ 7162£

Carte tipărită la comandă

Livrare economică 15-29 martie

Preluare comenzi: 021 569.72.76

Specificații

ISBN-13: 9783659134753
ISBN-10: 3659134759
Pagini: 220
Dimensiuni: 152 x 229 x 13 mm
Greutate: 0.33 kg
Editura: LAP LAMBERT ACADEMIC PUBLISHING AG & CO KG
Colecția LAP Lambert Academic Publishing

Notă biografică

Obtained a BSc in mathematics and a PhD in computer science. He worked as a researcher at Imperial College in collaboration with Microsoft Research Cambridge in a joint project on systems biology, and at The Microsoft Research - University of Trento COSBI. His main research interests include proof theory, formal methods and their applications.