Conference Paper/Proceeding/Abstract 1301 views
Uniform Schemata for Proof Rules
,
Tie Hou
Computability in Europe 2015 (CiE 2015), Volume: 8493, Pages: 53 - 62
Swansea University Author:
Ulrich Berger
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...
| 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!
|
| 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. |
|---|---|
| Keywords: |
Proof calculi, Semantics and logic of computation, Realizability |
| College: |
Faculty of Science and Engineering |
| Start Page: |
53 |
| End Page: |
62 |