Increasing the efficiency of automated theorem proving

uncategorised

Authors

Gabriel Aguilera

Inma P. de Guzmán

Manuel Ojeda-Aciego

Published

1 January 1995

Publication details

J. Appl. Non Class. Logics vol. 5 (1), pages 9–29.

Links

Abstract

ABSTRACT In this work a new Automated Theorem Prover (ATP) via refutation for classical logic and which does not require the conversion to clausal form, named TAS-D++, is introduced. The main objective in the design of this ATP was to obtain a parallel and computationally efficient method naturally extensible to non-standard logics (concretely, to temporal logics, see [12]). TAS-D++ works by using transformations of the syntactic trees of the formulas and, as tableaux and matrix style provers [6, 15, 16], it is Gentzen-based. Its power is mainly based in the efficient extraction of implicit information in the syntactic trees (in difference with the standard ATPs via refutation) to detect both: • simultaneously unsatisfiable or equivalent formulas to that being studied • valid, unsatisfiable, equivalent or equal subformulas. TAS-D++ is sound and complete and, moreover, it is a method that generates countermodels in a natural way.

Citation

Please, cite this work as:

[AGO95] G. Aguilera, I. P. de Guzmán, and M. Ojeda-Aciego. “Increasing the efficiency of automated theorem proving”. In: J. Appl. Non Class. Logics 5.1 (1995), pp. 9-29. DOI: 10.1080/11663081.1995.10510841. URL: https://doi.org/10.1080/11663081.1995.10510841.

BibTeX

@Article{Aguilera1995,
     author = {Gabriel Aguilera and Inman P. {de Guzm{’a}n} and Manuel Ojeda-Aciego},
     journal = {J. Appl. Non Class. Logics},
     title = {Increasing the efficiency of automated theorem proving},
     year = {1995},
     number = {1},
     pages = {9–29},
     volume = {5},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/journals/jancl/AguileraGO95.bib},
     doi = {10.1080/11663081.1995.10510841},
     timestamp = {Fri, 26 May 2023 01:00:00 +0200},
     url = {https://doi.org/10.1080/11663081.1995.10510841},
}

Bibliometric data

The following data has been extracted from resources such as OpenAlex, Dimensions, PlumX or Altmetric.

Increasing the efficiency of automated theorem proving

Cites

The following graph plots the number of cites received by this work from its publication, on a yearly basis.

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, M. Ojeda-Aciego, et al. “Reducing signed propositional formulas”. In: Soft Computing - A Fusion of Foundations, Methodologies and Applications 2.4 (Feb. 1999), p. 157–166. ISSN: 1433-7479. DOI: 10.1007/s005000050048. URL: http://dx.doi.org/10.1007/s005000050048.

[2] E. Altamirano and G. Escalada-Imaz. “An Efficient Proof Method for Non-clausal Reasoning”. In: Foundations of Intelligent Systems. Springer Berlin Heidelberg, 2000, p. 534–542. ISBN: 9783540399636. DOI: 10.1007/3-540-39963-1_56. URL: http://dx.doi.org/10.1007/3-540-39963-1_56.

[3] E. Altamirano and G. Escalada-Imaz. “Finding Tractable Formulas in NNF”. In: Computational Logic — CL 2000. Springer Berlin Heidelberg, 2000, p. 493–507. ISBN: 9783540449577. DOI: 10.1007/3-540-44957-4_33. URL: http://dx.doi.org/10.1007/3-540-44957-4_33.

[4] 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.

[5] G. Gutiérrez, I. P. de Guzmán, J. Martínez, et al. “Reduction Theorems for Boolean Formulas Using Δ-Trees”. In: Logics in Artificial Intelligence. Springer Berlin Heidelberg, 2000, p. 179–192. ISBN: 9783540400066. DOI: 10.1007/3-540-40006-0_13. URL: http://dx.doi.org/10.1007/3-540-40006-0_13.

[6] I. de Guzmán, M. Ojeda‐Aciego, and A. Valverde. “Implicates and reduction techniques for temporal logics”. In: Annals of Mathematics and Artificial Intelligence 27.1–4 (Apr. 1999), p. 3–23. ISSN: 1573-7470. DOI: 10.1023/a:1018923315631. URL: http://dx.doi.org/10.1023/a:1018923315631.

[7] I. P. de Guzmán, P. Cordero, and M. Enciso. “Structure Theorems for Closed Sets of Implicates/Implicants in Temporal Logic”. In: Progress in Artificial Intelligence. Springer Berlin Heidelberg, 1999, p. 193–207. ISBN: 9783540481591. DOI: 10.1007/3-540-48159-1_14. URL: http://dx.doi.org/10.1007/3-540-48159-1_14.

[8] I. P. de Guzmán, M. Ojeda-Aciego, and A. Valverde. “Implicates and Reduction Techniques for Temporal Logics”. In: Logics in Artificial Intelligence. Springer Berlin Heidelberg, 1998, p. 309–323. ISBN: 9783540495451. DOI: 10.1007/3-540-49545-2_21. URL: http://dx.doi.org/10.1007/3-540-49545-2_21.

[9] R. Hähnle. “Advanced Many-Valued Logics”. In: Handbook of Philosophical Logic. Springer Netherlands, 2001, p. 297–395. ISBN: 9789401704526. DOI: 10.1007/978-94-017-0452-6_5. URL: http://dx.doi.org/10.1007/978-94-017-0452-6_5.

[10] U. Hustadt. Resolution-based decision procedures for subclasses of first-order logic. En. 1999. DOI: 10.22028/D291-25703. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/25759.

[11] G. E. Imaz. “A first polynomial non-clausal class in many-valued logic”. In: Fuzzy Sets and Systems 456 (Mar. 2023), p. 1–37. ISSN: 0165-0114. DOI: 10.1016/j.fss.2022.10.008. URL: http://dx.doi.org/10.1016/j.fss.2022.10.008.