Deduction graphs with universal quantification

J.H. Geuvers, I. Loeb

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

Abstract

Deduction Graphs are meant to generalise both Gentzen-Prawitz style natural deductions and Fitch style flag deductions. They have the structure of acyclic directed graphs with boxes. In [Herman Geuvers and Iris Loeb. Natural Deduction via Graphs: Formal Definition and Computation Rules. Mathematical Structures in Computer Science (Special Issue on Theory and Applications of Term Graph Rewriting), Volume 17(03):485–526, 2007.] we have investigated the deduction graphs for minimal proposition logic. This paper studies the extension with first-order universal quantification, showing the robustness of the concept of deduction graphs.
Original languageEnglish
Title of host publicationProceedings 4th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2007, Braga, Portugal, March 31, 2007)
EditorsI. Mackie, D. Plump
Pages93-108
DOIs
Publication statusPublished - 2008

Publication series

NameElectronic Notes in Theoretical Computer Science
Volume203(1)
ISSN (Print)1571-0061

Fingerprint

Dive into the research topics of 'Deduction graphs with universal quantification'. Together they form a unique fingerprint.

Cite this