TAS-D({}^{}): Syntactic Trees Transformations for Automated Theorem Proving
Abstract
Citation
Please, cite this work as:
[AGO94] G. Aguilera, I. P. de Guzmán, and M. Ojeda-Aciego. “TAS-D(^++): Syntactic Trees Transformations for Automated Theorem Proving”. In: Logics in Artificial Intelligence, European Workshop, JELIA ’94, York, UK, September 5-8, 1994, Proceedings. Ed. by C. MacNish, D. Pearce and L. Pereira. Vol. 838. Lecture Notes in Computer Science. Springer, 1994, pp. 198-216. DOI: 10.1007/BFB0021973. URL: https://doi.org/10.1007/BFb0021973.
Papers citing this work
The following is a non-exhaustive list of papers that cite this work:
[1] G. Aguilera, I. P. de Guzmán, and M. Ojeda. “Increasing the efficiency of automated theorem proving”. In: Journal of Applied Non-Classical Logics 5.1 (Jan. 1995), p. 9–29. ISSN: 1958-5780. DOI: 10.1080/11663081.1995.10510841. URL: http://dx.doi.org/10.1080/11663081.1995.10510841.
[2] P. Cordero, M. Enciso, and I. P. de Guzmán. “A temporal negative normal form which preserves implicants and implicates”. In: Journal of Applied Non-Classical Logics 10.3–4 (Jan. 2000), p. 243–272. ISSN: 1958-5780. DOI: 10.1080/11663081.2000.10510999. URL: http://dx.doi.org/10.1080/11663081.2000.10510999.
[3] M. Enciso, I. P. Guzmán, and C. Rossi. “Temporal reasoning over linear discrete time”. In: Logics in Artificial Intelligence. Springer Berlin Heidelberg, 1996, p. 303–319. ISBN: 9783540706434. DOI: 10.1007/3-540-61630-6_22. URL: http://dx.doi.org/10.1007/3-540-61630-6_22.