[ Pobierz całość w formacie PDF ]
G : ~~A imp A
1. ! ! b c. [ | b : ~~A R G b c | ] ==> c : A
We now apply monl and dispose of the second subgoal using the rule starc, given
above in the declaration of the theory MR.
> by ( (rtac monl 1) THEN ( rtac starc 2))
G : ~~A imp A
1. ! ! b c. [ | b : ~~A R G b c | ] ==> c** : A
Next we apply rules as in the proof in Section 2.4 (atac proves a subgoal by
assumption after solving for unknowns).
> by ( EVERY [ rtac incEc 1, rtac negE 1, atac 2])
G : ~~A imp A
1. ! ! b c. [ | b : ~~A R G b c c* : ~A | ] ==> c : ~~A
> by ( rtac monl 1)
G : ~~A imp A
1. ! ! b c. [ | b : ~~A R G b c c* : ~A | ] ==> ?a5( b, c) : ~~A
2. ! ! b c. [ | b : ~~A R G b c c* : ~A | ] ==> R G ?a5( b, c) c
This leaves us with two subgoals, which are both proved by assumption, simpli-
fying ?a5(b, c) to b. Since no unproved subgoals remain, Isabelle reports that
we are nished.
> by ( REPEAT (atac 1))
G : ~~A imp A
No subgoals!
A.2 Correctness
By reasoning about our encoding and the metalogic M we can prove that,
e.g., MR corresponds to the original R. We do this in two parts, by showing
34
rst adequacy, that any proof in R can be reconstructed in MR, and then
faithfulness, that we can recover from any derivation in MR a proof in R itself.
Adequacy is easy to show, because the rules of R map directly onto the
axioms of MR. A simple inductive argument on the structure of proofs in R
establishes this, cf. [5, x5.2]. Faithfulness is more complex, since there is no
such simple mapping in this direction: arbitrary derivations in MR do not map
directly onto proofs in R. Instead we use proof-theoretic properties of M: any
derivation in M is equivalent to another in a (expanded) normal form [5, 40, 43].
Thus, given a derivation in MR we can, by induction over its normal form, nd
a derivation in R. This establishes faithfulness (again cf. [5, x5.2]). Moreover,
this proof is constructive: it not only tells us that there is a proof in R, it also
provides an e ective method for nding one.
Acknowledgements
We thank Andreas Nonnengart and an anonymous referee for helpful comments.
References
[1] A. R. Anderson, N. D. Belnap, Jr., and J. M. Dunn. Entailment, The
Logic of Relevance and Necessity, volume 2. Princeton University Press,
Princeton, New Jersey, 1992.
[2] A. Avron. Simple consequence relations. Information and Computation,
92:105{139, 1991.
[3] A. Avron, F. Honsell, M. Miculan, and C. Paravano. Encoding modal logics
in logical frameworks. Studia Logica, 1997. This issue.
[4] D. Basin, S. Matthews, and L. Vigan o. Implementing modal and relevance
logics in a logical framework. In L. Carlucci Aiello, J. Doyle, and S. Shapiro,
editors, Proceedings of KR' 96, pages 386{397. Morgan Kaufmann Publish-
ers, Inc., San Francisco, California, 1996.
[5] D. Basin, S. Matthews, and L. Vigan o. Labelled propositional modal logics:
theory and practice. Journal of Logic and Computation, 1997. To appear.
[6] N. D. Belnap, Jr. Display logic. Journal of Philosophical Logic, 11:357{417,
1982.
[7] R. Bull and K. Segerberg. Basic Modal Logic, pages 1{88. Volume 2 of
Gabbay and Guenthner [19], 1984.
[8] M. D'Agostino and D. M. Gabbay. A generalization of analytic deduction
via labelled deductive systems. Part I : basic substructural logics. Journal
of Automated Reasoning, 13:243{281, 1994.
[9] K. Do sen. Sequent-systems for modal logic. Journal of Symbolic Logic,
50(1):149{168, 1985.
35
[10] K. Do sen. Negation as a modal operator. Reports on Mathematical Logic,
20:15{27, 1986.
[11] M. Dummett. The philosophical basis of intuitionistic logic. In Truth
and other enigmas, pages 215{247. Harvard University Press, Cambridge,
Massachusetts, 1978.
[12] J. M. Dunn. Relevance Logic and Entailment, pages 117{224. Volume 3 of
Gabbay and Guenthner [19], 1986.
[13] J. M. Dunn. Star and perp: Two treatments of negation. In J. Tomberlin,
editor, Philosophical Perspectives, volume 7, pages 331{357. Ridgeview,
Atascadero, California, 1994.
[14] J. M. Dunn. Gaggle theory applied to modal, intuitionistic, and relevance
logics. In I. Max and W. Stelzner, editors, Logik und Mathematik (Frege
Kolloquium ' 93), pages 335{368. de Gruyter, Berlin, 1995.
[15] J. M. Dunn. Positive modal logic. Studia Logica, 55:301{317, 1995.
[16] L. Farinas Del Cerro and A. Herzig. Combining classical and intuitionistic
~
logic. In F. Baader and K. U. Schulz, editors, Frontiers of Combining
Systems, pages 93{102. Kluwer Academic Publishers, Dordrecht, 1996.
[17] M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Kluwer
Academic Publishers, Dordrecht, 1983.
[18] D. M. Gabbay. LDS { Labelled Deductive Systems (Volume 1 - Founda-
tions). Clarendon Press, Oxford, 1996.
[19] D. M. Gabbay and F. Guenthner, editors. Handbook of Philosophical Logic.
D. Reidel Publishing Company, Dordrecht, 1983{1986.
[20] P. Gardner. A new type theory for representing logics. In A. Voronkov,
editor, Proceedings ofLPAR' 93, LNAI 698, pages 146{157. Springer, Berlin,
1993.
[21] P. Gardner. Equivalences between logics and their representing type theo-
ries. Mathematical Structures in Computer Science, 5:323{349, 1995.
[22] G. Gentzen. Untersuchungen uber das logische Schlie en I, II. Mathe-
matische Zeitschrift, 39:176{210, 405{431, 1934{1935. English translation
in [23].
[23] G. Gentzen. Investigations into logical deduction. In M. Szabo, editor,
The collected papers of Gerhard Gentzen, pages 68{131. North Holland,
Amsterdam, 1969.
[24] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1{102, 1987.
36
[25] R. Goldblatt. Semantical analysis of orthologic. Journal of Philosophical
Logic, 3:19{35, 1974.
[26] R. Harper, F. Honsell, and G. Plotkin. A framework for de ning logics.
Journal of the ACM, 40(1):143{184, 1993.
[27] A. Herzig. Raisonnement Automatique en Logique Modale et Algorithmes
d' Uni cation. PhD thesis, Universit e Paul-Sabatier, Toulouse, 1989.
[28] F. Honsell and M. Miculan. A natural deduction approach to dynamic
logics. In S. Berardi and M. Coppo, editors, Proceedings of TYPES' 95,
LNCS 1158, pages 165{182. Springer, Berlin, 1996.
[29] G. Hughes and M. Cresswell. A companion to modal logic. Methuen, Lon-
don, 1984.
[30] I. Humberstone. Interval semantics for tense logic: Some remarks. Journal
of Philosophical Logic, 8:171{196, 1979.
[31] B. J onsson and A. Tarski. Boolean algebras with operators. American
Journal of Mathematics, 73{4:891{939, 127{162, 1951-52.
[32] S. Martini and A. Masini. A computational interpretation of modal proofs.
In H. Wansing, editor, Proof Theory of Modal Logic, pages 213{241. Kluwer
Academic Publishers, Dordrecht, 1996.
[33] A. Masini. 2-sequent calculus: a proof theory of modalities. Annals of Pure
and Applied Logic, 58:229{246, 1992.
[34] R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer, editors. Selected Papers
on Automath. Elsevier, Amsterdam, 1994.
[35] H. J. Ohlbach. A Resolution Calculus for Modal Logics. PhD thesis, Uni-
versit Kaiserslautern, Kaiserslautern, Germany, 1988.
at
[36] H. J. Ohlbach. Translation methods for non-classical logics: an overview.
Bulletin o f the IGPL, 1(1):69{90, 1993.
[37] E. Orlowska. Relational interpretation of modal logics. In H. Andr eka, J. D.
Monk, and I. N emeti, editors, Algebraic Logic. North-Holland, Amsterdam,
1991.
[38] E. Orlowska. Relational proof system for relevant logics. Journal of Sym-
bolic Logic, 57(4):1425{1440, 1992.
[39] L. Paulson. The foundation of a generic theorem prover. Journal o f Auto-
mated Reasoning, 5:363{397, 1989.
[ Pobierz całość w formacie PDF ]
zanotowane.pldoc.pisz.plpdf.pisz.plalternate.pev.pl
|
