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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
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