Name
Abstract | ||
|---|---|---|
We define the notions of a canonical inference rule and a canonical constructive system in the framework of strict single-conclusion
Gentzen-type systems (or, equivalently, natural deduction systems), and develop a corresponding general non-deterministic
Kripke-style semantics. We show that every constructive canonical system induces a class of non-deterministic Kripke-style
frames, for which it is strongly sound and complete. This non-deterministic semantics is used to show that such a system always
admits a strong form of the cut-elimination theorem, and for providing a decision procedure for such systems.
|
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-02716-1_6 | Analytic Tableaux and Related Methods |
Keywords | Field | DocType |
non-deterministic semantics,constructive canonical system,corresponding general non-deterministic kripke-style,canonical constructive systems,decision procedure,non-deterministic kripke-style frame,canonical inference rule,strict single-conclusion gentzen-type system,cut-elimination theorem,canonical constructive system,natural deduction system,type system,inference rule,natural deduction | Atomic formula,Intuitionistic logic,Discrete mathematics,Horn clause,Constructive,Natural deduction,Computer science,Algorithm,Rule of inference,Semantics | Conference |
Volume | ISSN | Citations |
5607 | 0302-9743 | 1 |
PageRank | References | Authors |
0.40 | 7 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Arnon Avron | 1 | 1292 | 147.65 |
| Ori Lahav | 2 | 252 | 23.53 |