×

An automata view to goal-directed methods. (English) Zbl 1485.68144

Drewes, Frank (ed.) et al., Language and automata theory and applications. 11th international conference, LATA 2017, Umeå, Sweden, March 6–9, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10168, 103-114 (2017).
Summary: Consequence-based and automata-based algorithms encompass two families of approaches that have been thoroughly studied as reasoning methods for many logical formalisms. While automata are useful for finding tight complexity bounds, consequence-based algorithms are typically simpler to describe, implement, and optimize. In this paper, we show that consequence-based reasoning can be reduced to the emptiness test of an appropriately built automaton. Thanks to this reduction, one can focus on developing efficient consequence-based algorithms, obtaining complexity bounds and other benefits of automata methods for free.
For the entire collection see [Zbl 1358.68010].

MSC:

68Q45 Formal languages and automata
68T27 Logic in artificial intelligence

Software:

ELK; LTL2BA
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Baader, F., Brandt, S., Lutz, C.: Pushing the \[ \mathcal{EL} \] envelope. In: Proceedings of IJCAI 2005. Morgan Kaufmann, Edinburgh (2005)
[2] Baader, F., Hladik, J., Peñaloza, R.: Automata can show PSPACE results for description logics. Inf. Comput. 206(9–10), 1045–1056 (2008) · Zbl 1149.68073 · doi:10.1016/j.ic.2008.03.006
[3] Baader, F., Knechtel, M., Peñaloza, R.: Context-dependent views to axioms and consequences of semantic web ontologies. J. Web Semant. 12–13, 22–40 (2012) · doi:10.1016/j.websem.2011.11.006
[4] Baader, F., Peñaloza, R.: Automata-based axiom pinpointing. J. Autom. Reason. 45(2), 91–129 (2010) · Zbl 1213.68589 · doi:10.1007/s10817-010-9181-2
[5] Baader, F., Peñaloza, R.: Axiom pinpointing in general tableaux. J. Log. Comput. 20(1), 5–34 (2010) · Zbl 1191.68645 · doi:10.1093/logcom/exn058
[6] Baader, F., Peñaloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic \[ \mathcal{EL}^+ \] . In: Hertzberg, J., Beetz, M., Englert, R. (eds.) KI 2007. LNCS (LNAI), vol. 4667, pp. 52–67. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-74565-5_7 · Zbl 05364420 · doi:10.1007/978-3-540-74565-5_7
[7] Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun. 25(2), 97–116 (2012) · Zbl 1248.68450
[8] Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034
[9] Dividino, R.Q., Schenk, S., Sizov, S., Staab, S.: Provenance, trust, explanations - and all that other meta knowledge. KI 23(2), 24–30 (2009)
[10] Droste, M., Gastin, P.: Weighted automata and weighted logics. Theoret. Comput. Sci. 380(1–2), 69–86 (2007) · Zbl 1118.68076 · doi:10.1016/j.tcs.2007.02.055
[11] Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001). doi: 10.1007/3-540-44585-4_6 · Zbl 0991.68044 · doi:10.1007/3-540-44585-4_6
[12] Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL DL entailments. In: Aberer, K., et al. (eds.) ASWC/ISWC -2007. LNCS, vol. 4825, pp. 267–280. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-76298-0_20 · Zbl 05246846 · doi:10.1007/978-3-540-76298-0_20
[13] Kazakov, Y.: Consequence-driven reasoning for Horn SHIQ ontologies. In: Boutilier, C. (ed.) Proceedings of IJCAI 2009, pp. 2040–2045 (2009)
[14] Kazakov, Y., Krötzsch, M., Simančík, F.: The incredible ELK: from polynomial procedures to efficient reasoning with \[ \mathcal{E\!L} \] ontologies. J. Autom. Reason. 53, 1–61 (2014) · Zbl 1331.68216 · doi:10.1007/s10817-013-9296-3
[15] Kleine Büning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Handbook of Satisfiability, pp. 339–401 (2009)
[16] Kullmann, O.: Investigations on autark assignments. Discret. Appl. Math. 107(1–3), 99–137 (2000) · Zbl 0965.03018 · doi:10.1016/S0166-218X(00)00262-6
[17] Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 22–35. Springer, Heidelberg (2006). doi: 10.1007/11814948_4 · Zbl 1187.68552 · doi:10.1007/11814948_4
[18] Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2016) · Zbl 1334.90080 · doi:10.1007/s10601-015-9183-0
[19] Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557–580 (2007) · Zbl 1112.68116 · doi:10.1016/j.ic.2006.08.009
[20] Peñaloza, R.: Using sums-of-products for non-standard reasoning. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 488–499. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-13089-2_41 · Zbl 1284.68534 · doi:10.1007/978-3-642-13089-2_41
[21] Riguzzi, F., Bellodi, E., Lamma, E., Zese, R.: Probabilistic description logics under the distribution semantics. Semant. Web 6(5), 477–501 (2015) · Zbl 1400.68226 · doi:10.3233/SW-140154
[22] Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: Proceedings of IJCAI 2003, pp. 355–362. Morgan Kaufmann (2003)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.