TAS-D({}^{}): Syntactic Trees Transformations for Automated Theorem Proving

uncategorised
Authors
Published

1 January 1994

Publication details

Logics in Artificial Intelligence, European Workshop, {JELIA} ’94, York, UK, September 5-8, 1994, Proceedings , Lecture Notes in Computer Science vol. 838, pages 198–216.

Links

DOI

 

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.

@InProceedings{Aguilera1994a,
     author = {Gabriel Aguilera and Inman P. {de Guzm{’a}n} and Manuel Ojeda-Aciego},
     booktitle = {Logics in Artificial Intelligence, European Workshop, {JELIA} ’94, York, UK, September 5-8, 1994, Proceedings},
     title = {TAS-D({}^{}): Syntactic Trees Transformations for Automated Theorem Proving},
     year = {1994},
     editor = {Craig MacNish and David Pearce and Lu'Moniz Pereira},
     pages = {198–216},
     publisher = {Springer},
     series = {Lecture Notes in Computer Science},
     volume = {838},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/conf/jelia/AguileraGO94.bib},
     doi = {10.1007/BFB0021973},
     timestamp = {Fri, 26 May 2023 01:00:00 +0200},
     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.