Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

2015 | OriginalPaper | Chapter

Spatial Symmetry Driven Pruning Strategies for Efficient Declarative Spatial Reasoning

Authors: Carl Schultz, Mehul Bhatt

Published in: Spatial Information Theory

Publisher: Springer International Publishing

share
SHARE

Abstract

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.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Testen Sie jetzt 15 Tage kostenlos.

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




Testen Sie jetzt 15 Tage kostenlos.

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Testen Sie jetzt 15 Tage kostenlos.

Footnotes
1
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.
 
2
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.
 
3
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].
 
4
Spatial Reasoning (CLP(QS)). www.​spatial-reasoning.​com.
 
5
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.
 
6
That is, constructive methods may fail in building a consistent solution, and iterative root finding methods may fail to converge.
 
7
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.
 
8
All cases have been verified using Reduce as presented in Theorem 2.
 
Literature
1.
go back to reference 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.
go back to reference 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
4.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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
20.
go back to reference 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.
go back to reference 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
23.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
32.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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)
Metadata
Title
Spatial Symmetry Driven Pruning Strategies for Efficient Declarative Spatial Reasoning
Authors
Carl Schultz
Mehul Bhatt
Copyright Year
2015
DOI
https://doi.org/10.1007/978-3-319-23374-1_16

Premium Partner