Abstract
Based on an analysis of the inference rules used, we provide a characterization of the situations in which classical provability entails intuitionistic provability. We then examine the relationship of these derivability notions to uniform provability, a restriction of intuitionistic provability that embodies a special form of goal-directedness. We determine, first, the circumstances in which the former relations imply the latter. Using this result, we identify the richest versions of the so-called abstract logic programming languages in classical and intuitionistic logic. We then study the reduction of classical and, derivatively, intuitionistic provability to uniform provability via the addition to the assumption set of the negation of the formula to be proved. Our focus here is on understanding the situations in which this reduction is achieved. However, our discussions indicate the structure of a proof procedure based on the reduction, a matter also considered explicitly elsewhere.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 273-298 |
| Number of pages | 26 |
| Journal | Theoretical Computer Science |
| Volume | 232 |
| Issue number | 1-2 |
| DOIs | |
| State | Published - Feb 6 2000 |
Bibliographical note
Funding Information:We are grateful for comments received from the anonymous reviewers of this paper; the careful reading and detailed suggestions of one of these reviewers have led to several improvements in presentation. We also acknowledge helpful comments provided by Michael J. O’Donnell. This work has been supported in part by NSF Grants CCR-92-08465 and CCR-9596119.
Keywords
- Classical logic
- Intuitionistic logic
- Logic programming
- Proof search
- Proof theory
- Uniform provability