Abstract
Partial functions are ubiquitous in Knowledge Representation applications, ranging from practical, e.g., business applications, to more abstract, e.g., mathematical and programming applications. Expressing propositions about partial functions may lead to non/denoting terms resulting in undefinedness errors and ambiguity, causing subtle modeling and reasoning problems.
In our approach, formulas are well-defined (true or false) and non/ambiguous in all structures. We develop a base extension of three/valued predicate logic, in which partial function terms are guarded by domain expressions ensuring the well/definedness property despite the three/valued nature of the underlying logic. To tackle the verbosity of this core language, we propose different ways to increase convenience by using disambiguating annotations and non/commutative connectives. We show a reduction of the logic to two/valued logic of total functions and prove that many different unnesting methods turning partial functions into graph predicates, which are not equivalence preserving in general, are equivalence preserving in the proposed language, showing that ambiguity is avoided.
This work was partially supported by the Flemish Government under the “Onderzoeksprogramma Artificiële Intelligentie (AI) Vlaanderen”.
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
Similar content being viewed by others
Notes
- 1.
Ver/1 and Col/1 are denoting the set of vertices and colours respectively, Nei/2 is neighbourhood relation, and function colOf/1 is mapping objects to their colour.
- 2.
Grice’s principle of cooperativity explains that the human interpretation of a text is influenced by a subconscious desire to make good sense of it.
- 3.
Note that every structure with the same domain interpreters “\(=\)” as the same relation. All other language built-in relations and functions are to be interpreted in the same way. Note that in the case of partial functions their domain predicate would also be interpreted (e.g., division/would come with \(\delta _/\) that is true for all pairs of numbers \((x_1,x_2)\) such that \(x_2 \ne 0\).
- 4.
It is also possible to move undefined values into the structure and then just manipulate it in the evaluation function. However, we choose to stay close to the standard set/theoretic implementation of concepts.
- 5.
The total expansion of a structure does not satisfy the constraints of a partial function structure (Definition 4).
- 6.
The notation for operators is selected to be aligned with the intuition of modal operators, i.e., \(\pmb {[[}\pmb {]]}\) expresses the necessity that all terms are defined, while \(\pmb {\langle \langle } \pmb {\rangle \rangle }\) expresses possibility.
- 7.
We use constants F for France, B for blue and R for red.
- 8.
Recall that the graph predicate of a function f is denoted with \(\gamma _f\).
- 9.
The proof is omitted due to space constraints.
- 10.
Weak unnesting becomes strong when the formula occurs in a negative context (odd number of negations upper in syntax tree). This can cause problems, i.e., some connectives (e.g., \(\Leftrightarrow \)) contain implicit negations, and hence polarity is not well defined.
References
Balduccini, M.: A “conservative’’ approach to extending answer set programming with non-Herbrand functions. In: Erdem, E., Lee, J., Lierler, Y., Pearce, D. (eds.) Correct Reasoning. LNCS, vol. 7265, pp. 24–39. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30743-0_3
Balduccini, M.: ASP with non-Herbrand partial functions: a language and system for practical use. Theory Pract. Logic Program. 13(4–5), 547–561 (2013)
Berezin, S., Barrett, C., Shikanian, I., Chechik, M., Gurfinkel, A., Dill, D.L.: A practical approach to partial functions in CVC lite. Electron. Notes Theor. Comput. Sci. 125(3), 13–23 (2005)
Cabalar, P.: Partial functions and equality in answer set programming. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 392–406. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89982-2_36
Cristiá, M., Rossi, G., Frydman, C.S.: Adding partial functions to Constraint Logic Programming with sets. Theory Pract. Log. Program. 15, 651–665 (2015)
De Cat, B., Bogaerts, B., Bruynooghe, M., Janssens, G., Denecker, M.: Predicate logic as a modeling language: the IDP system. In: Declarative Logic Programming: Theory, Systems, and Applications, pp. 279–323. Association for Computing Machinery and Morgan & Claypool (2018)
Farmer, W.M.: A partial functions version of Church’s simple theory of types. J. Symb. Log. 55(3), 1269–1291 (1990)
Fitting, M.: Kleene’s three valued logics and their children. Fundam. Inform. 20(1, 2, 3), 113–131 (1994)
Frisch, A.M., Stuckey, P.J.: The proper treatment of undefinedness in constraint languages. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 367–382. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04244-7_30
Gavilanes-Franco, A., Lucio-Carrasco, F.: A first order logic for partial functions. Theoret. Comput. Sci. 74(1), 37–69 (1990)
Gomes, C.P., Sabharwal, A., Selman, B.: Model counting. In: Handbook of Satisfiability, pp. 993–1014. IOS press (2021)
Hoang, T.S.: An introduction to the Event-B modelling method. Industr. Deploy. Syst. Eng. Methods 211–236 (2013)
Kleene, S.C.: Introduction to Metamathematics. North Holland, Princeton (1952)
Lonsing, F., Egly, U.: Evaluating QBF solvers: quantifier alternations matter. In: Hooker, J. (ed.) CP 2018. LNCS, vol. 11008, pp. 276–294. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98334-9_19
McCarthy, J.: A basis for a mathematical theory of computation. In: Studies in Logic and the Foundations of Mathematics, vol. 26, pp. 33–70. Elsevier (1959)
McCarthy, J.: Elaboration tolerance. In: Common Sense, vol. 98, p. 2 (1998)
Mitchell, D., Ternovska, E., Hach, F., Mohebali, R.: Model expansion as a framework for modelling and solving search problems. Technical report, Citeseer (2006)
Nivelle, H.: Classical logic with partial functions. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 203–217. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_18
Rabe, M.N., Seshia, S.A.: Incremental determinization. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 375–392. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_23
Russell, B.: On denoting. Mind 14(56), 479–493 (1905)
Schock, R.: Logics Without Existence Assumptions. Stockholm, Almqvist & Wiksell, Stockholm (1968)
Scott, D.: Identity and existence in intuitionistic logic. In: Fourman, M., Mulvey, C., Scott, D. (eds.) Applications of Sheaves. LNM, vol. 753, pp. 660–696. Springer, Heidelberg (1979). https://doi.org/10.1007/BFb0061839
Strawson, P.F.: On referring. Mind 59(235), 320–344 (1950)
Suppes, P.: Introduction to Logic. Courier Corporation (1999)
Wittocx, J., Mariën, M., Denecker, M.: Grounding FO and FO(ID) with bounds. J. Artif. Intell. Res. 38, 223–269 (2010)
Acknowledgements
Thanks to Pierre Carbonnelle, Gerda Janssens, Linde Vanbesien, and Marcos Cramer for the discussions and for reading this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Markovic, D., Bruynooghe, M., Denecker, M. (2023). Towards Systematic Treatment of Partial Functions in Knowledge Representation. In: Gaggl, S., Martinez, M.V., Ortiz, M. (eds) Logics in Artificial Intelligence. JELIA 2023. Lecture Notes in Computer Science(), vol 14281. Springer, Cham. https://doi.org/10.1007/978-3-031-43619-2_51
Download citation
DOI: https://doi.org/10.1007/978-3-031-43619-2_51
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-43618-5
Online ISBN: 978-3-031-43619-2
eBook Packages: Computer ScienceComputer Science (R0)