No Cover Image

Conference Paper/Proceeding/Abstract 1272 views

Uniform Schemata for Proof Rules

Ulrich Berger Orcid Logo, Tie Hou

Computability in Europe 2015 (CiE 2015), Volume: 8493, Pages: 53 - 62

Swansea University Author: Ulrich Berger Orcid Logo

Full text not available from this repository: check for access using links below.

DOI (Published version): 10.1007/978-3-319-08019-2

Abstract

Motivated by the desire to facilitate the implementation of interactive proof systems with rich sets of proof rules, we present a uniform system of rule schemata to generate proof rules for different styles of logical calculi. The system requires only one schema for each logical operator to generate...

Full description

Published in: Computability in Europe 2015 (CiE 2015)
Published: Cham, Heidelberg, New York, Dordrecht, London Springer 2014
Online Access: http://link.springer.com/chapter/10.1007/978-3-319-08019-2_6
URI: https://cronfa.swan.ac.uk/Record/cronfa21691
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2015-05-27T02:10:53Z
last_indexed 2018-02-09T04:59:29Z
id cronfa21691
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2016-11-08T00:45:04.1259874</datestamp><bib-version>v2</bib-version><id>21691</id><entry>2015-05-26</entry><title>Uniform Schemata for Proof Rules</title><swanseaauthors><author><sid>61199ae25042a5e629c5398c4a40a4f5</sid><ORCID>0000-0002-7677-3582</ORCID><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2015-05-26</date><deptcode>SCS</deptcode><abstract>Motivated by the desire to facilitate the implementation of interactive proof systems with rich sets of proof rules, we present a uniform system of rule schemata to generate proof rules for different styles of logical calculi. The system requires only one schema for each logical operator to generate introduction and elimination rules in natural deduction and sequent calculus style. In addition, the system supports program extraction from proofs by generating realizers for the proof rules automatically.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Computability in Europe 2015 (CiE 2015)</journal><volume>8493</volume><paginationStart>53</paginationStart><paginationEnd>62</paginationEnd><publisher>Springer</publisher><placeOfPublication>Cham, Heidelberg, New York, Dordrecht, London</placeOfPublication><keywords>Proof calculi, Semantics and logic of computation, Realizability</keywords><publishedDay>23</publishedDay><publishedMonth>6</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-06-23</publishedDate><doi>10.1007/978-3-319-08019-2</doi><url>http://link.springer.com/chapter/10.1007/978-3-319-08019-2_6</url><notes></notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2016-11-08T00:45:04.1259874</lastEdited><Created>2015-05-26T13:45:25.1227071</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>1</order></author><author><firstname>Tie</firstname><surname>Hou</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2016-11-08T00:45:04.1259874 v2 21691 2015-05-26 Uniform Schemata for Proof Rules 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2015-05-26 SCS Motivated by the desire to facilitate the implementation of interactive proof systems with rich sets of proof rules, we present a uniform system of rule schemata to generate proof rules for different styles of logical calculi. The system requires only one schema for each logical operator to generate introduction and elimination rules in natural deduction and sequent calculus style. In addition, the system supports program extraction from proofs by generating realizers for the proof rules automatically. Conference Paper/Proceeding/Abstract Computability in Europe 2015 (CiE 2015) 8493 53 62 Springer Cham, Heidelberg, New York, Dordrecht, London Proof calculi, Semantics and logic of computation, Realizability 23 6 2014 2014-06-23 10.1007/978-3-319-08019-2 http://link.springer.com/chapter/10.1007/978-3-319-08019-2_6 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2016-11-08T00:45:04.1259874 2015-05-26T13:45:25.1227071 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Tie Hou 2
title Uniform Schemata for Proof Rules
spellingShingle Uniform Schemata for Proof Rules
Ulrich Berger
title_short Uniform Schemata for Proof Rules
title_full Uniform Schemata for Proof Rules
title_fullStr Uniform Schemata for Proof Rules
title_full_unstemmed Uniform Schemata for Proof Rules
title_sort Uniform Schemata for Proof Rules
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
Tie Hou
format Conference Paper/Proceeding/Abstract
container_title Computability in Europe 2015 (CiE 2015)
container_volume 8493
container_start_page 53
publishDate 2014
institution Swansea University
doi_str_mv 10.1007/978-3-319-08019-2
publisher Springer
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://link.springer.com/chapter/10.1007/978-3-319-08019-2_6
document_store_str 0
active_str 0
description Motivated by the desire to facilitate the implementation of interactive proof systems with rich sets of proof rules, we present a uniform system of rule schemata to generate proof rules for different styles of logical calculi. The system requires only one schema for each logical operator to generate introduction and elimination rules in natural deduction and sequent calculus style. In addition, the system supports program extraction from proofs by generating realizers for the proof rules automatically.
published_date 2014-06-23T03:25:46Z
_version_ 1763750913761083392
score 11.028886

Similar Items