Abstract
We propose Logical Problem Solving Framework (LPSF), an axiomatic structure for generating methods of logical problem solving. Input parameters of LPSF consist of (1) a canonical logical structure, (2) a set of equivalent transformation rules (ET rules), (3) a control, and (4) an answer mapping. Given these input parameters, LPSF provides a logical problem solver, which receives an original problem, sets an initial state in a formula on the logical structure, makes a computation path, and if the computation path reaches the domain of the answer mapping, it outputs an answer, which is guaranteed to be correct. By taking input parameters such as KR-Logic, a set of extended clauses obtained through meaning-preserving Skolemization, ET rules including unfolding in the extended clause-set space constructed on KR-Logic, we can solve, with strict guarantee of correctness, a larger class of logical problems, compared to conventional methods.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Akama, K., Nantajeewarawat, E.: Meaning-preserving Skolemization. In: 3rd International Conference on Knowledge Engineering and Ontology Development, Paris, France, pp. 322–327 (2011)
Akama, K., Nantajeewarawat, E.: Equivalent transformation in an extended space for solving query-answering problems. In: Nguyen, N.T., Attachoo, B., Trawiński, B., Somboonviwat, K. (eds.) ACIIDS 2014. LNCS (LNAI), vol. 8397, pp. 232–241. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05476-6_24
Akama, K., Nantajeewarawat, E.: Model-intersection problems with existentially quantified function variables: formalization and a solution schema. In: 8th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management, Porto, Portugal, vol. 2, pp. 52–63 (2016)
Akama, K., Nantajeewarawat, E.: Solving query-answering problems with constraints for function variables. In: Nguyen, N.T., Hoang, D.H., Hong, T.-P., Pham, H., Trawiński, B. (eds.) ACIIDS 2018. LNCS (LNAI), vol. 10751, pp. 36–47. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75417-8_4
Akama, K., Nantajeewarawat, E., Akama, T.: Computation control by prioritized ET rules. In: 10th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management, KEOD, Seville, Spain, vol. 2, pp. 84–95 (2018)
Akama, K., Nantajeewarawat, E., Akama, T.: Side-change transformation. In: 10th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management, KEOD, Seville, Spain, vol. 2, pp. 237–246 (2018)
Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, Cambridge (1973)
Donini, F.M., Lenzerini, M., Nardi, D., Schaerf, A.: \(\cal{AL}\)-log: integrating datalog and description logics. J. Intell. Coop. Inf. Syst. 10, 227–252 (1998)
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987). https://doi.org/10.1007/978-3-642-83189-8
Motik, B., Sattler, U., Studer, R.: Query answering for OWL-DL with rules. J. Web Semant. 3, 41–60 (2005)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12, 23–41 (1965)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Akama, K., Nantajeewarawat, E., Akama, T. (2019). Logical Problem Solving Framework. In: Nguyen, N., Gaol, F., Hong, TP., Trawiński, B. (eds) Intelligent Information and Database Systems. ACIIDS 2019. Lecture Notes in Computer Science(), vol 11431. Springer, Cham. https://doi.org/10.1007/978-3-030-14799-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-14799-0_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-14798-3
Online ISBN: 978-3-030-14799-0
eBook Packages: Computer ScienceComputer Science (R0)