Theories and Tools

HOL Theory for A generative algebra for spatio-temporal information

The Isabelle/HOL theory that accompanies the paper Modelling spatio-temporal information generation is found here

R package mss

A prototypical R package for meaningful spatial statistics is found here. It defines fields, entities and aggregations for spatial (not spatio-temporal) data. A vignette demonstrating its use is found here.

HOL Theory for Meaningful Spatial Prediction and Aggregation

The theory for meaningful spatial prediction and aggregation has been formalised in Higher-Order-Logic and implemented and proved in Isabelle/HOL, a semi-automated theorem prover. The theory is available here.

OWL Pattern

An ontology pattern written in the Web Ontology Language (OWL) is available to to annotate datasets and statistical methods and link them with statistical methods. This allows to implement a recommender tool for statistical methods on datasets, as shown in a prototypical implementation for the R software.

Resources:

R script for Meaningful Spatial Statistics

In order to demonstrate the potential of using the variable types defined in our theory for implementing a recommender tool, we have written an R script, that extends classes from the sp package in R and uses type checks to allow or disallow interpolations or aggregations. The script can be downloaded here.

Annotation Portal

We have a first version of a Web portal online that allows to add metadata about meaningful analysis and publish this as linked open data.
http://www.geographicknowledge.de/vocab/AlgebraReferenceSystems.thy

HOL Theory for Meaningful Spatial Prediction and Aggregation

The theory for meaningful spatial prediction and aggregation has been formalised in Higher-Order-Logic and implemented and proved in Isabelle/HOL, a semi-automated theorem prover. The theory is available here.

OWL Pattern

An ontology pattern written in the Web Ontology Language (OWL) is available to to annotate datasets and statistical methods and link them with statistical methods. This allows to implement a recommender tool for statistical methods on datasets, as shown in a prototypical implementation for the R software.

Resources:

R script for Meaningful Spatial Statistics

In order to demonstrate the potential of using the variable types defined in our theory for implementing a recommender tool, we have written an R script, that extends classes from the sp package in R and uses type checks to allow or disallow interpolations or aggregations. The script can be downloaded here.

Annotation Portal

We have a first version of a Web portal online that allows to add metadata about meaningful analysis and publish this as linked open data.