Reductions for non-clausal theorem proving

uncategorised

Authors

Gabriel Aguilera

Inma P. de Guzmán

Manuel Ojeda-Aciego

Agustín Valverde

Published

1 January 2001

Publication details

Theor. Comput. Sci. vol. 266 (1-2), pages 81–112.

Links

Abstract

Citation

Please, cite this work as:

[Agu+01] G. Aguilera, I. P. de Guzmán, M. Ojeda-Aciego, et al. “Reductions for non-clausal theorem proving”. In: Theor. Comput. Sci. 266.1-2 (2001), pp. 81-112. DOI: 10.1016/S0304-3975(00)00044-X. URL: https://doi.org/10.1016/S0304-3975(00)00044-X.

BibTeX

@Article{Aguilera2001,
     author = {Gabriel Aguilera and Inman P. {de Guzm{’a}n} and Manuel Ojeda-Aciego and Agust'Valverde},
     journal = {Theor. Comput. Sci.},
     title = {Reductions for non-clausal theorem proving},
     year = {2001},
     number = {1-2},
     pages = {81–112},
     volume = {266},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/journals/tcs/AguileraGOV01.bib},
     doi = {10.1016/S0304-3975(00)00044-X},
     timestamp = {Fri, 26 May 2023 01:00:00 +0200},
     url = {https://doi.org/10.1016/S0304-3975(00)00044-X},
}

Bibliometric data

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

Citations
CrossRef - Citation Indexes: 11
Scopus - Citation Indexes: 15

Captures
Mendeley - Readers: 5

See more details

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-Venegas, J. L. Galán-García, M. á. Galán-García, et al. “Teaching Semantic Tableaux Method for Propositional Classical Logic with a CAS”. In: International Journal for Technology in Mathematics Education 22.2 (Jun. 2015), p. 85–91. ISSN: 1744-2710. DOI: 10.1564/tme_v22.2.07. URL: http://dx.doi.org/10.1564/tme_v22.2.07.

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

[3] P. Cordero, M. Enciso, and I. de Guzmán. “Bases for closed sets of implicants and implicates in temporal logic”. In: Acta Informatica 38.9 (Aug. 2002), p. 599–619. ISSN: 1432-0525. DOI: 10.1007/s00236-002-0087-2. URL: http://dx.doi.org/10.1007/s00236-002-0087-2.

[4] P. Cordero, G. Gutiérrez, J. Martínez, et al. “A New Algebraic Tool for Automatic Theorem Provers”. In: Annals of Mathematics and Artificial Intelligence 42.4 (Dec. 2004), p. 369–398. ISSN: 1012-2443. DOI: 10.1023/b:amai.0000038312.77514.3c. URL: http://dx.doi.org/10.1023/b:amai.0000038312.77514.3c.

[5] M. Ferrari, C. Fiorentini, and G. Fiorino. “Simplification Rules for Intuitionistic Propositional Tableaux”. In: ACM Transactions on Computational Logic 13.2 (Apr. 2012), p. 1–23. ISSN: 1557-945X. DOI: 10.1145/2159531.2159536. URL: http://dx.doi.org/10.1145/2159531.2159536.

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

[7] I. de Guzmán, M. Ojeda-Aciego, and A. Valverde. “Restricted Δ-Trees in Multiple-Valued Logics”. In: Artificial Intelligence: Methodology, Systems, and Applications. Springer Berlin Heidelberg, 2002, p. 223–232. ISBN: 9783540461487. DOI: 10.1007/3-540-46148-5_23. URL: http://dx.doi.org/10.1007/3-540-46148-5_23.

[8] I. P. de Guzmán, M. Ojeda-Aciego, and A. Valverde. “Restricted Δ-Trees and Reduction Theorems in Multiple-Valued Logics”. In: Advances in Artificial Intelligence — IBERAMIA 2002. Springer Berlin Heidelberg, 2002, p. 161–171. ISBN: 9783540361312. DOI: 10.1007/3-540-36131-6_17. URL: http://dx.doi.org/10.1007/3-540-36131-6_17.

[9] X. He, Y. Xu, J. Liu, et al. “α-Generalized lock resolution method in linguistic truth-valued lattice-valued logic”. In: International Journal of Computational Intelligence Systems 5.6 (2012), p. 1120. ISSN: 1875-6883. DOI: 10.1080/18756891.2012.747665. URL: http://dx.doi.org/10.1080/18756891.2012.747665.

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

[11] J. Ma, W. Li, D. Ruan, et al. “Filter-based resolution principle for lattice-valued propositional logic LP(X)”. In: Information Sciences 177.4 (Feb. 2007), p. 1046–1062. ISSN: 0020-0255. DOI: 10.1016/j.ins.2006.07.027. URL: http://dx.doi.org/10.1016/j.ins.2006.07.027.

[12] F. J. Martín-Mateos, J. A. Alonso, M. J. Hidalgo, et al. “Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers”. In: Logic Based Program Synthesis and Transformation. Springer Berlin Heidelberg, 2003, p. 182–198. ISBN: 9783540450139. DOI: 10.1007/3-540-45013-0_15. URL: http://dx.doi.org/10.1007/3-540-45013-0_15.

[13] J. Martínez, G. Gutiérrez, I. de Guzmán, et al. “Generalizations of lattices via non-deterministic operators”. In: Discrete Mathematics 295.1–3 (May. 2005), p. 107–141. ISSN: 0012-365X. DOI: 10.1016/j.disc.2004.08.043. URL: http://dx.doi.org/10.1016/j.disc.2004.08.043.

[14] M. Ojeda-Aciego and A. Valverde. “tascpl: TAS Solver for Classical Propositional Logic”. In: Logics in Artificial Intelligence. Springer Berlin Heidelberg, 2004, p. 738–741. ISBN: 9783540302278. DOI: 10.1007/978-3-540-30227-8_70. URL: http://dx.doi.org/10.1007/978-3-540-30227-8_70.

[15] D. Pearce, I. P. de Guzmán, and A. Valverde. “Computing Equilibrium Models Using Signed Formulas”. In: Computational Logic — CL 2000. Springer Berlin Heidelberg, 2000, p. 688–702. ISBN: 9783540449577. DOI: 10.1007/3-540-44957-4_46. URL: http://dx.doi.org/10.1007/3-540-44957-4_46.

[16] Y. Xu, J. Liu, X. Zhong, et al. “Multiary α-Resolution Principle for a Lattice-Valued Logic”. In: IEEE Transactions on Fuzzy Systems 21.5 (Oct. 2013), p. 898–912. ISSN: 1941-0034. DOI: 10.1109/tfuzz.2012.2236095. URL: http://dx.doi.org/10.1109/tfuzz.2012.2236095.

[17] X. Zhong, Y. Xu, J. Liu, et al. “General form of α-resolution principle for linguistic truth-valued lattice-valued logic”. In: Soft Computing 16.10 (Jun. 2012), p. 1767–1781. ISSN: 1433-7479. DOI: 10.1007/s00500-012-0860-2. URL: http://dx.doi.org/10.1007/s00500-012-0860-2.