2015 | OriginalPaper | Buchkapitel
Tipp
Weitere Kapitel dieses Buchs durch Wischen aufrufen
Erschienen in:
Spatial Information Theory
Declarative spatial reasoning denotes the ability to (declaratively) specify and solve real-world problems related to geometric and qualitative spatial representation and reasoning within standard knowledge representation and reasoning (KR) based methods (e.g., logic programming and derivatives). One approach for encoding the semantics of spatial relations within a declarative programming framework is by systems of polynomial constraints. However, solving such constraints is computationally intractable in general (i.e. the theory of real-closed fields).
We present a new algorithm, implemented within the declarative spatial reasoning system CLP(QS), that drastically improves the performance of deciding the consistency of spatial constraint graphs over conventional polynomial encodings. We develop pruning strategies founded on spatial symmetries that form equivalence classes (based on affine transformations) at the qualitative spatial level. Moreover, pruning strategies are themselves formalised as knowledge about the properties of space and spatial symmetries. We evaluate our algorithm using a range of benchmarks in the class of contact problems, and proofs in mereology and geometry. The empirical results show that CLP(QS) with knowledge-based spatial pruning outperforms conventional polynomial encodings by orders of magnitude, and can thus be applied to problems that are otherwise unsolvable in practice.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
Anzeige
1
2
3
4
5
6
7
8
Incompleteness refers to the inability of a spatial reasoning method to determine whether a given network of qualitative spatial constraints is consistent or inconsistent in general. Relation-algebraic spatial reasoning (i.e. using algebraic closure based on weak composition) has been shown to be incomplete for a number of spatial languages and cannot guarantee
consistency in general, e.g. relative directions [
23] and containment relations between linearly ordered intervals [
22], Theorem 5.9.
We emphasise that this analytic geometry approach that we also adopt is not
qualitative spatial reasoning in the relation algebraic sense; the foundations are similar (i.e. employing a finite language of spatial relations that are interpreted as infinite sets of configurations, determining consistency in the complete absence of numeric information, and so on) but the methods for determining consistency etc. come from different branches of spatial reasoning.
Standard geometric constraint languages of approaches including [
12,
17,
27] consist of points, lines, circles, ellipses, and coincidence, tangency, perpendicularity, parallelism, and numerical dimension constraints; note the absence of e.g. mereotopology and “common-sense” relative orientation relations [
35].
Spatial Reasoning (CLP(QS)).
www.spatial-reasoning.com.
Important factors in determining the applicability of various analytic approaches are the degree of the polynomials (particularly the distinction between linear and nonlinear) and whether both equality and inequalities are permitted in the constraints.
That is, constructive methods may fail in building a consistent solution, and iterative root finding methods may fail to converge.
The properties of affine transformations and the geometric objects that they preserve are well understood; further information is readily available in introductory texts such as [
26]. Our key contribution is formalising and exploiting this spatial knowledge as modular and extensible common-sense rules in intelligent knowledge-based spatial assistance systems.
All cases have been verified using Reduce as presented in Theorem
2.
1.
Zurück zum Zitat Aiello, M., Pratt-Hartmann, I.E., van Benthem, J.F.: Handbook of Spatial Logics. Springer-Verlag New York Inc., Secaucus (2007). ISBN 978-1-4020-5586-7 CrossRefMATH Aiello, M., Pratt-Hartmann, I.E., van Benthem, J.F.: Handbook of Spatial Logics. Springer-Verlag New York Inc., Secaucus (2007). ISBN 978-1-4020-5586-7
CrossRefMATH
2.
Zurück zum Zitat Arnon, D.S., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition I: the basic algorithm. SIAM J. Comput. 13(4), 865–877 (1984) CrossRefMathSciNetMATH Arnon, D.S., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition I: the basic algorithm. SIAM J. Comput.
13(4), 865–877 (1984)
CrossRefMathSciNetMATH
3.
Zurück zum Zitat Bhatt, M., Wallgrün, J.O.: Geospatial narratives and their spatio-temporal dynamics: Commonsense reasoning for high-level analyses in geographic information systems. ISPRS Int. J. Geo-Information 3(1), 166–205 (2014). doi: 10.3390/ijgi3010166. http://dx.doi.org/10.3390/ijgi3010166 CrossRef Bhatt, M., Wallgrün, J.O.: Geospatial narratives and their spatio-temporal dynamics: Commonsense reasoning for high-level analyses in geographic information systems. ISPRS Int. J. Geo-Information
3(1), 166–205 (2014). doi:
10.3390/ijgi3010166.
http://dx.doi.org/10.3390/ijgi3010166
CrossRef
4.
Zurück zum Zitat Bhatt, M., Lee, J.H., Schultz, C.: CLP(QS): a declarative spatial reasoning framework. In: Egenhofer, M., Giudice, N., Moratz, R., Worboys, M. (eds.) COSIT 2011. LNCS, vol. 6899, pp. 210–230. Springer, Heidelberg (2011) CrossRef Bhatt, M., Lee, J.H., Schultz, C.: CLP(QS): a declarative spatial reasoning framework. In: Egenhofer, M., Giudice, N., Moratz, R., Worboys, M. (eds.) COSIT 2011. LNCS, vol. 6899, pp. 210–230. Springer, Heidelberg (2011)
CrossRef
5.
Zurück zum Zitat Bhatt, M., Schultz, C., Freksa, C.: The ‘Space’ in spatial assistance systems: conception, formalisation and computation. In: Tenbrink, T., Wiener, J., Claramunt, C. (eds.) Representing space in cognition: Interrelations of behavior, language, and formal models. Series: Explorations in Language and Space. Oxford University Press (2013). 978-0-19-967991-1 Bhatt, M., Schultz, C., Freksa, C.: The ‘Space’ in spatial assistance systems: conception, formalisation and computation. In: Tenbrink, T., Wiener, J., Claramunt, C. (eds.) Representing space in cognition: Interrelations of behavior, language, and formal models. Series: Explorations in Language and Space. Oxford University Press (2013). 978-0-19-967991-1
6.
Zurück zum Zitat Bhatt, M., Suchan, J., Schultz, C.: Cognitive interpretation of everyday activities - toward perceptual narrative based visuo-spatial scene interpretation. In: Finlayson, M., Fisseni, B., Loewe, B., Meister, J.C. (eds.) Computational Models of Narrative (CMN) 2013, a satellite workshop of CogSci 2013: The 35th meeting of the Cognitive Science Society., Dagstuhl, Germany, OpenAccess Series in Informatics (OASIcs) (2013) Bhatt, M., Suchan, J., Schultz, C.: Cognitive interpretation of everyday activities - toward perceptual narrative based visuo-spatial scene interpretation. In: Finlayson, M., Fisseni, B., Loewe, B., Meister, J.C. (eds.) Computational Models of Narrative (CMN) 2013, a satellite workshop of CogSci 2013: The 35th meeting of the Cognitive Science Society., Dagstuhl, Germany, OpenAccess Series in Informatics (OASIcs) (2013)
7.
Zurück zum Zitat Bhatt, M., Schultz, C.P.L., Thosar, M.: Computing narratives of cognitive user experience for building design analysis: KR for industry scale computer-aided architecture design. In: Baral, C., Giacomo, G.D., Eiter, T. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, KR 2014, Vienna, Austria, 20–24 July, 2014. AAAI Press (2014). ISBN 978-1-57735-657-8 Bhatt, M., Schultz, C.P.L., Thosar, M.: Computing narratives of cognitive user experience for building design analysis: KR for industry scale computer-aided architecture design. In: Baral, C., Giacomo, G.D., Eiter, T. (eds.) Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, KR 2014, Vienna, Austria, 20–24 July, 2014. AAAI Press (2014). ISBN 978-1-57735-657-8
8.
Zurück zum Zitat Borgo, S.: Spheres, cubes and simplexes in mereogeometry. Logic Logical Philos. 22(3), 255–293 (2013) MATH Borgo, S.: Spheres, cubes and simplexes in mereogeometry. Logic Logical Philos.
22(3), 255–293 (2013)
MATH
9.
Zurück zum Zitat Bouhineau, D.: Solving geometrical constraint systems using CLP based on linear constraint solver. In: Pfalzgraf, J., Calmet, J., Campbell, J. (eds.) AISMC 1996. LNCS, vol. 1138, pp. 274–288. Springer, Heidelberg (1996) CrossRef Bouhineau, D.: Solving geometrical constraint systems using CLP based on linear constraint solver. In: Pfalzgraf, J., Calmet, J., Campbell, J. (eds.) AISMC 1996. LNCS, vol. 1138, pp. 274–288. Springer, Heidelberg (1996)
CrossRef
10.
Zurück zum Zitat Bouhineau, D., Trilling, L., Cohen, J.: An application of CLP: Checking the correctness of theorems in geometry. Constraints 4(4), 383–405 (1999) CrossRefMathSciNetMATH Bouhineau, D., Trilling, L., Cohen, J.: An application of CLP: Checking the correctness of theorems in geometry. Constraints
4(4), 383–405 (1999)
CrossRefMathSciNetMATH
11.
Zurück zum Zitat Buchberger, B.: Bruno Buchberger’s PhD thesis 1965: an algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal (English translation). J. Symbolic Comput. 41(3), 475–511 (2006) CrossRefMathSciNetMATH Buchberger, B.: Bruno Buchberger’s PhD thesis 1965: an algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal (English translation). J. Symbolic Comput.
41(3), 475–511 (2006)
CrossRefMathSciNetMATH
12.
Zurück zum Zitat Chou, S.-C.: Mechanical Geometry Theorem Proving, vol. 41. Springer Science and Business Media, Dordrecht (1988) MATH Chou, S.-C.: Mechanical Geometry Theorem Proving, vol. 41. Springer Science and Business Media, Dordrecht (1988)
MATH
13.
Zurück zum Zitat Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975) Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)
14.
Zurück zum Zitat Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symbolic Comput. 12(3), 299–328 (1991). ISSN 0747–7171 CrossRefMathSciNetMATH Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symbolic Comput.
12(3), 299–328 (1991). ISSN 0747–7171
CrossRefMathSciNetMATH
15.
Zurück zum Zitat Dolzmann, A., Seidl, A., Sturm, T.: REDLOG User Manual, Edition 3.0, Apr 2004 Dolzmann, A., Seidl, A., Sturm, T.: REDLOG User Manual, Edition 3.0, Apr 2004
16.
Zurück zum Zitat Gantner, Z., Westphal, M., Wölfl, S.: GQR-A fast reasoner for binary qualitative constraint calculi. In: Proceedings of AAAI, vol. 8 (2008) Gantner, Z., Westphal, M., Wölfl, S.: GQR-A fast reasoner for binary qualitative constraint calculi. In: Proceedings of AAAI, vol. 8 (2008)
17.
Zurück zum Zitat Hadas, N., Hershkowitz, R., Schwarz, B.B.: The role of contradiction and uncertainty in promoting the need to prove in dynamic geometry environments. Educ. Stud. Mathe. 44(1–2), 127–150 (2000) CrossRef Hadas, N., Hershkowitz, R., Schwarz, B.B.: The role of contradiction and uncertainty in promoting the need to prove in dynamic geometry environments. Educ. Stud. Mathe.
44(1–2), 127–150 (2000)
CrossRef
18.
Zurück zum Zitat Haunold, P., Grumbach, S., Kuper, G., Lacroix, Z.: Linear constraints: Geometric objects represented by inequalitiesl. In: Frank, A.U. (ed.) COSIT 1997. LNCS, vol. 1329, pp. 429–440. Springer, Heidelberg (1997) CrossRef Haunold, P., Grumbach, S., Kuper, G., Lacroix, Z.: Linear constraints: Geometric objects represented by inequalitiesl. In: Frank, A.U. (ed.) COSIT 1997. LNCS, vol. 1329, pp. 429–440. Springer, Heidelberg (1997)
CrossRef
19.
Zurück zum Zitat Jaffar, J., Maher, M.J.: Constraint logic programming: A survey. J. Logic Prog. 19, 503–581 (1994) CrossRefMathSciNet Jaffar, J., Maher, M.J.: Constraint logic programming: A survey. J. Logic Prog.
19, 503–581 (1994)
CrossRefMathSciNet
20.
Zurück zum Zitat Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. In: Rosenkrantz, D.J., Sagiv, Y. (eds.) Proceedings of the Ninth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, Nashville, Tennessee, USA, 2–4 April, 1990, pp. 299–313. ACM Press (1990). ISBN 0-89791-352-3 Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. In: Rosenkrantz, D.J., Sagiv, Y. (eds.) Proceedings of the Ninth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, Nashville, Tennessee, USA, 2–4 April, 1990, pp. 299–313. ACM Press (1990). ISBN 0-89791-352-3
21.
Zurück zum Zitat Kapur, D., Mundy, J.L. (eds.): Geometric Reasoning. MIT Press, Cambridge (1988). ISBN 0-262-61058-2 MATH Kapur, D., Mundy, J.L. (eds.): Geometric Reasoning. MIT Press, Cambridge (1988). ISBN 0-262-61058-2
MATH
22.
Zurück zum Zitat Ladkin, P.B., Maddux, R.D.: On binary constraint problems. J. ACM (JACM) 41(3), 435–469 (1994) CrossRefMathSciNetMATH Ladkin, P.B., Maddux, R.D.: On binary constraint problems. J. ACM (JACM)
41(3), 435–469 (1994)
CrossRefMathSciNetMATH
23.
Zurück zum Zitat Lee, J.H.: The complexity of reasoning with relative directions. In: 21st European Conference on Artificial Intelligence (ECAI 2014) (2014) Lee, J.H.: The complexity of reasoning with relative directions. In: 21st European Conference on Artificial Intelligence (ECAI 2014) (2014)
24.
Zurück zum Zitat Ligozat, G.: Qualitative Spatial and Temporal Reasoning. Wiley-ISTE, Hoboken (2011) MATH Ligozat, G.: Qualitative Spatial and Temporal Reasoning. Wiley-ISTE, Hoboken (2011)
MATH
25.
Zurück zum Zitat Ligozat, G.F.: Qualitative triangulation for spatial reasoning. In: Campari, I., Frank, A.U. (eds.) COSIT 1993. LNCS, vol. 716, pp. 54–68. Springer, Heidelberg (1993) Ligozat, G.F.: Qualitative triangulation for spatial reasoning. In: Campari, I., Frank, A.U. (eds.) COSIT 1993. LNCS, vol. 716, pp. 54–68. Springer, Heidelberg (1993)
26.
Zurück zum Zitat Martin, G.E.: Transformation geometry: An introduction to symmetry. Springer, New York (1982) CrossRefMATH Martin, G.E.: Transformation geometry: An introduction to symmetry. Springer, New York (1982)
CrossRefMATH
27.
Zurück zum Zitat Owen, J.C.: Algebraic solution for geometry from dimensional constraints. In: Proceedings of the First ACM Symposium on Solid Modeling Foundations and CAD/CAM Applications, pp. 397–407. ACM (1991) Owen, J.C.: Algebraic solution for geometry from dimensional constraints. In: Proceedings of the First ACM Symposium on Solid Modeling Foundations and CAD/CAM Applications, pp. 397–407. ACM (1991)
28.
Zurück zum Zitat Pesant, G., Boyer, M.: QUAD-CLP (R): Adding the power of quadratic constraints. In: Borning, A. (ed.) PPCP 1994. LNCS, vol. 874, pp. 95–108. Springer, Heidelberg (1994) CrossRef Pesant, G., Boyer, M.: QUAD-CLP (R): Adding the power of quadratic constraints. In: Borning, A. (ed.) PPCP 1994. LNCS, vol. 874, pp. 95–108. Springer, Heidelberg (1994)
CrossRef
29.
Zurück zum Zitat Pesant, G., Boyer, M.: Reasoning about solids using constraint logic programming. J. Automated Reasoning 22(3), 241–262 (1999) CrossRefMATH Pesant, G., Boyer, M.: Reasoning about solids using constraint logic programming. J. Automated Reasoning
22(3), 241–262 (1999)
CrossRefMATH
30.
Zurück zum Zitat Randell, D.A., Cohn, A.G., Cui Z.: Computing transitivity tables: A challenge for automated theorem provers. In 11th International Conference on Automated Deduction (CADE-11), pp. 786–790 (1992) Randell, D.A., Cohn, A.G., Cui Z.: Computing transitivity tables: A challenge for automated theorem provers. In 11th International Conference on Automated Deduction (CADE-11), pp. 786–790 (1992)
31.
Zurück zum Zitat Ratschan, S.: Approximate quantified constraint solving by cylindrical box decomposition. Reliable Comput. 8(1), 21–42 (2002) CrossRefMathSciNetMATH Ratschan, S.: Approximate quantified constraint solving by cylindrical box decomposition. Reliable Comput.
8(1), 21–42 (2002)
CrossRefMathSciNetMATH
32.
Zurück zum Zitat Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Logic (TOCL) 7(4), 723–748 (2006) CrossRefMathSciNet Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Logic (TOCL)
7(4), 723–748 (2006)
CrossRefMathSciNet
33.
Zurück zum Zitat Schultz, C., Bhatt, M.: Towards a declarative spatial reasoning system. In: 20th European Conference on Artificial Intelligence (ECAI 2012) (2012) Schultz, C., Bhatt, M.: Towards a declarative spatial reasoning system. In: 20th European Conference on Artificial Intelligence (ECAI 2012) (2012)
34.
Zurück zum Zitat Schultz, C., Bhatt, M.: Declarative spatial reasoning with boolean combinations of axis-aligned rectangular polytopes. In: ECAI 2014–21st European Conference on Artificial Intelligence, pp. 795–800 (2014) Schultz, C., Bhatt, M.: Declarative spatial reasoning with boolean combinations of axis-aligned rectangular polytopes. In: ECAI 2014–21st European Conference on Artificial Intelligence, pp. 795–800 (2014)
35.
Zurück zum Zitat Schultz, C., Bhatt, M., Borrmann, A.: Bridging qualitative spatial constraints and parametric design - a use case with visibility constraints. In: EG-ICE: 21st International Workshop - Intelligent Computing in Engineering 2014 (2014) Schultz, C., Bhatt, M., Borrmann, A.: Bridging qualitative spatial constraints and parametric design - a use case with visibility constraints. In: EG-ICE: 21st International Workshop - Intelligent Computing in Engineering 2014 (2014)
36.
Zurück zum Zitat Tarski, A.: A general theorem concerning primitive notions of Euclidean geometry. Indagationes Mathematicae 18(468), 74 (1956) Tarski, A.: A general theorem concerning primitive notions of Euclidean geometry. Indagationes Mathematicae
18(468), 74 (1956)
37.
Zurück zum Zitat Varzi, A.C.: Parts, wholes, and part-whole relations: The prospects of mereotopology. Data Knowl. Eng. 20(3), 259–286 (1996) CrossRefMATH Varzi, A.C.: Parts, wholes, and part-whole relations: The prospects of mereotopology. Data Knowl. Eng.
20(3), 259–286 (1996)
CrossRefMATH
38.
Zurück zum Zitat Walega, P., Bhatt, M., Schultz, C.: ASPMT(QS): non-monotonic spatial reasoning with answer set programming modulo theories. In: LPNMR: Logic Programming and Nonmonotonic Reasoning - 13th International Conference (2015). http://lpnmr2015.mat.unical.it Walega, P., Bhatt, M., Schultz, C.: ASPMT(QS): non-monotonic spatial reasoning with answer set programming modulo theories. In: LPNMR: Logic Programming and Nonmonotonic Reasoning - 13th International Conference (2015).
http://lpnmr2015.mat.unical.it
39.
Zurück zum Zitat Wallgrün, J.O., Frommberger, L., Wolter, D., Dylla, F., Freksa, C.: Qualitative spatial representation and reasoning in the SparQ-Toolbox. In: Barkowsky, T., Knauff, M., Ligozat, G., Montello, D.R. (eds.) Spatial Cognition 2007. LNCS (LNAI), vol. 4387, pp. 39–58. Springer, Heidelberg (2007) CrossRef Wallgrün, J.O., Frommberger, L., Wolter, D., Dylla, F., Freksa, C.: Qualitative spatial representation and reasoning in the SparQ-Toolbox. In: Barkowsky, T., Knauff, M., Ligozat, G., Montello, D.R. (eds.) Spatial Cognition 2007. LNCS (LNAI), vol. 4387, pp. 39–58. Springer, Heidelberg (2007)
CrossRef
40.
Zurück zum Zitat Wenjun, W.: Basic principles of mechanical theorem proving in elementary geometries. J. Syst. Sci. Math. Sci. 4(3), 207–235 (1984) Wenjun, W.: Basic principles of mechanical theorem proving in elementary geometries. J. Syst. Sci. Math. Sci.
4(3), 207–235 (1984)
- Titel
- Spatial Symmetry Driven Pruning Strategies for Efficient Declarative Spatial Reasoning
- DOI
- https://doi.org/10.1007/978-3-319-23374-1_16
- Autoren:
-
Carl Schultz
Mehul Bhatt
- Sequenznummer
- 16