Abstract
Following the idea of Linear Proofs presented in [4] we introduce the Direct Logic [14] with exponentials (DLE). The logic combines Direct Logic with the exponentials of Linear Logic. For a well-chosen subclass of formulas of this logic we provide a matrix-characterization which can be used as a foundation for proof-search methods based on the connection calculus.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
G. Bellin, J. Ketonen. A decision procedure revisited: Notes on Direct Logic, Linear Logic and its implementation. Theoretical Computer Science, 95:115–142, 1992.
W. Bibel. On matrices with connections. Journal of the ACM, 28:633–645, 1981.
W. Bibel, L. Farinas del Cerro, B. Fronhöfer, A. Herzig. Plan Generation by Linear Proofs: On Semantics. In GWAI'89 13th German Workshop on Artificial Intelligence ed. D. Metzing, 49–62. Informatik-Fachberichte 216, Springer.
W. Bibel. A deductive solution for plan generation. New Generation Computing, 4:115–132, 1986.
G. Birkhoff. Lattice Theory. American Mathematical Society, New York, 1967.
S. Brüning, S. Hölldobler, J. Schneeberger, U. Sigmund, M. Thielscher. Disjunction in Resource-Oriented Deductive Planning. Technical Report AIDA-93-03, Intellektik, Informatik, TH-Darmstadt, 1994.
S. Cerrito. Herbrand Methods in Sequent Calculi: Unification in LL. Proceedings of the Joint International Conference and Symposium on Logic Programming, 607–621, 1992. 8. K. Dosen. A Historical Introduction to Substructural logics. In Substructural Logics ed. by K. Dosen and P. Schroeder-Heister. Oxford University Press, 1993.
B. Fronhöfer. The Action-as-Implication Paradigm. CS Press, München, 1996.
J. Gallier. Constructive Logics. Part II: Linear Logic and Proof Nets. Research Report PR2-RR-9, Digital Equipment Corporation, Paris, May 1991.
D. Galmiche, G. Perrier. On Proof Normalization in Linear Logic. Theoretical Computer Science, 135:67–110, 1994.
J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50:1–102, 1987.
G. Grosse, S. Hölldobler, J. Schneeberger. Linear deductive planning. Journal of Logic and Computation, 6:233–262, 1996.
J. Ketonen, R. Weyhrauch. A decidable fragment of predicate calculus. Theoretical Computer Science, 32:297–307, 1984.
A.P. Kopylov. Decidability of Linear Affine Logic. In Tenth Annual IEEE Symposium on Logic in Computer Science ed. by D. Kozen, 496–504, 1995.
C. Kreitz, H. Mantel, J. Otten, S. Schmitt. Connection-based proof construction in Linear Logic. CARE-14, 1997.
M. Massfron, C. Tollu, J. Vauzilles. Generating Plans in Linear Logic 1: Actions as Proofs. Theoretical Computer Science, 113: 349–370, 1993.
J. McCarthy, P.J. Hayes. Some Philosophical Problems from the Standpoint of Artificial Intelligence. Machine Intelligence, 4:463–502, 1969.
H. Ono. Semantics for Substructural Logics. In Substructural Logics ed. by K. Dosen and P. Schroeder-Heister. Oxford University Press, 1993.
N. Shankar. Proof Search in intuitionistic sequent calculus. CARE-11, 1992.
L. Wallen. Automated deduction in nonclassical logics. MIT Press, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sandner, E. (1997). From linear proofs to direct logic with exponentials. In: Brewka, G., Habel, C., Nebel, B. (eds) KI-97: Advances in Artificial Intelligence. KI 1997. Lecture Notes in Computer Science, vol 1303. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540634932_10
Download citation
DOI: https://doi.org/10.1007/3540634932_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63493-5
Online ISBN: 978-3-540-69582-0
eBook Packages: Springer Book Archive