Increasing the efficiency of automated theorem proving
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.
Bibliometric data
The following data has been extracted from resources such as OpenAlex, Dimensions, PlumX or Altmetric.
- Citations
- Scopus - Citation Indexes: 8
- Captures
- Mendeley - Readers: 4
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.