diff --git a/README.md b/README.md
index c55f20577dc21d4e184dbdcbfffa5f6e3f545b97..ad958abbd7776bc86660bb38398e514a4d4ea19c 100644
--- a/README.md
+++ b/README.md
@@ -16,9 +16,10 @@ Besides that, there is also
- [`IntegrationTests/`](./source/IntegrationTests): contains some integration tests run by the unit tests in the frameit-mmt submodule of the UniFormal/MMT project
-## Contributing
+## Documentation
-See [`Scrolls/README.md`](./source/Scrolls) for how to write scrolls.
+- [`./source/Scrolls/README.md`](./source/Scrolls) for a guide on how to write scrolls.
+- [`./situation-space.md`](./situation-space.md) for an overview how a situation space and theory looks like over the course of playing.
## Authors
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz
new file mode 100644
index 0000000000000000000000000000000000000000..9eaa82160a954bd1e5527e0b86005f8037e54fb8
Binary files /dev/null and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz differ
diff --git a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
index a003a310ddaac2945e140ceaaaa6d7e3db90d6b4..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
+++ b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
@@ -1,2 +0,0 @@
-<errors>
-</errors>
diff --git a/narration/IntegrationTests/SituationTheory.omdoc b/narration/IntegrationTests/SituationTheory.omdoc
index 6d8c720195aec95938fafd182738f9b26d82e8cb..1b100fcf3ec5621ceb0304b4780f80405f3d6eca 100644
--- a/narration/IntegrationTests/SituationTheory.omdoc
+++ b/narration/IntegrationTests/SituationTheory.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:2102.84.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld/integrationtests"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:220.6.26"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1535.56.0:1549.56.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1661.64.0:1681.64.20"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:1753.61.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test"/><instruction text="rule scala://parser.api.mmt.kwarc.info?MMTURILexer"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#271.7.0:291.7.20"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/relational/IntegrationTests/SituationTheory.rel b/relational/IntegrationTests/SituationTheory.rel
index 76d8127407b0963dc4b74adf8c8fd7c2a9179203..9e59fa8ed8d24ebc4c67bc2b3d281f4737050f83 100644
--- a/relational/IntegrationTests/SituationTheory.rel
+++ b/relational/IntegrationTests/SituationTheory.rel
@@ -1,4 +1,2 @@
document http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc
-Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace
-Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll
-Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel
new file mode 100644
index 0000000000000000000000000000000000000000..ce0b4250c6c19850dd5243e9e3dc615be1750e02
--- /dev/null
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel
@@ -0,0 +1,139 @@
+theory http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace?Root
+theory http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?OppositeLen
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?AngleSum
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?first_view
+HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view ☞frameworld:?OppositeLen/Problem
+HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root
+view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view
+HasViewFrom http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root ☞frameworld:?OppositeLen/Problem
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?A
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?A
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?B
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?B
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?C
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?C
diff --git a/situation-space.md b/situation-space.md
new file mode 100644
index 0000000000000000000000000000000000000000..fff662fd1e022ccfc32b16b1931dfb223aeee39c
--- /dev/null
+++ b/situation-space.md
@@ -0,0 +1,67 @@
+## The Evolution of a Situation Space
+
+This is an overview of how a situation space and theory looks like over the course of playing.
+
+Read from top to bottom; the comments indicate the "current" action that led to the creation of the respective module or declaration.
+
+```mmt
+
+fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
+
+theory SituationSpace =
+ // Player starts with situation_theory_1 below that includes this root situation theory,
+ providing access to scrolls that are available by default â™
+ theory Root =
+ include ☞http://mathhub.info/FrameIT/frameworld?OppositeLen â™
+ include ☞http://mathhub.info/FrameIT/frameworld?AngleSum â™
+ include ☞http://mathhub.info/FrameIT/frameworld?Midpoint â™
+ âš
+
+ // Player starts with this situation theory. â™
+ theory situation_theory_1 =
+ include ?DefaultSituationSpace/Root â™
+
+ // The player collects some facts about the world. â™
+ fact1: ... â™
+ fact2: ... â™
+ fact3: ... â™
+
+ // The player formulates a scroll view... (continued below) â™
+ view scroll_view_1 : ?OppositeLen/Problem -> ?SituationSpace/situation_theory_1 =
+ factslot1 = fact1 â™
+ factslot2 = fact2 â™
+ factslot3 = fact3 â™
+ âš
+ âš
+
+ // (continued)... and applies the scroll and thus lands in a new derived situation theory. â™
+ theory situation_theory_2 =
+ include ?SituationSpace/situation_theory_1 â™
+
+ // The player gets access to facts obtained by the scroll (these are precisely the ones pushed out
+ from ?OppositeLen/Solution over ?SituationSpace?situation_theory_1?scroll_view_1). â™
+ out_fact1: ... â™
+ out_fact2: ... â™
+ out_fact3: ... â™
+
+ // The player goes on collecting more facts. â™
+ fact4: ... â™
+ fact5: ... â™
+
+ // The player again formulates a scroll, now being able to combine facts they measured themselves
+ and facts they previously obtained via scroll application. â™
+ view scroll_view_2 : ?OppositeLen/Problem -> ?SituationSpace/situation_theory_2 =
+ factslot1 = out_fact1 â™
+ factslot2 = fact4 â™
+ factslot3 = out_fact3 â™
+ âš
+ âš
+
+ theory SituationSpace/situation_theory_3 =
+ include ?SituationSpace/situation_theory_2 â™
+ out_fact4: ... â™
+
+ // and so on and so forth â™
+ âš
+âš
+```
\ No newline at end of file
diff --git a/source/IntegrationTests/SituationTheory.mmt b/source/IntegrationTests/SituationTheory.mmt
index 4258dc07b611d6b23fed9e7c54cf29a89936125b..13d12a9c2fa1d1b66007e643ced38a2459c67235 100644
--- a/source/IntegrationTests/SituationTheory.mmt
+++ b/source/IntegrationTests/SituationTheory.mmt
@@ -1,10 +1,11 @@
-namespace http://mathhub.info/FrameIT/frameworld/integrationtests âš
+namespace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test âš
-import frameworld http://mathhub.info/FrameIT/frameworld âš
+rule scala://parser.api.mmt.kwarc.info?MMTURILexer âš
+import frameworld http://mathhub.info/FrameIT/frameworld âš
fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
-theory SampleSituationSpace =
+theory SituationSpace =
theory Root =
// planar triangle in R^2 â™
include ☞frameworld:?OppositeLen â™
@@ -34,52 +35,50 @@ theory SampleSituationSpace =
meta frameworld:?MetaAnnotations?label "ð”¹â„‚"
â™
- angleABC
+ angleB
: Σ β:â„. ⊦ ( ∠A,B,C ) ≠β â˜
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ â˜
meta frameworld:?MetaAnnotations?label "∠ð”¸ð”¹â„‚"
â™
- angleBAC
+ angleA
: Σ β:â„. ⊦ ( ∠B,A,C ) ≠β â˜
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ â˜
meta frameworld:?MetaAnnotations?label "∠ℬð”¸â„‚"
â™
- rightAngledC
+ rightAngleC
: ⊦ ( ∠B,C,A ) ≠90.0 â˜
= sketch "calculated by ComFreek by hand, hopefully correct" â˜
meta frameworld:?MetaAnnotations?label "∟ℂ"
â™
- âš
-âš
-theory MyScroll =
- theory Problem = a: type â™âš
- theory Solution =
- include ?MyScroll/Problem â™
- c: type ☠= aâ™
- âš
-âš
-
-theory SituationSpace =
- theory RootSituationTheory =
- include ?MyScroll â™
- b: type â™
- p : point ☠= ⟨0.0, 0.0, 0.0⟩ â™
-
- view v : ?MyScroll/Problem -> ?SituationSpace/RootSituationTheory =
- a = b â™
+ view first_view : frameworld:?OppositeLen/Problem -> ?SituationSpace/Root =
+ A = A â™
+ B = B â™
+ C = C â™
+ distanceBC = distanceBC â™
+ angleB = angleB â™
+ rightAngleC = rightAngleC â™
+ âš
âš
- âš
- theory PushedOutSituationTheory =
- include ?SituationSpace/RootSituationTheory â™
- c: type â™
- q = p â™
+ theory Derived1 =
+ include ?SituationSpace/Root â™
+ deducedLineCA : Σ x:â„ . ⊦ (d- C A) ≠x ☠= ⟨(tan (Ï€l angleB)) â‹… (Ï€l distanceBC), sketch "OppositeLen Scroll"⟩ â™
- view w : ?MyScroll/Problem -> ?SituationSpace/PushedOutSituationTheory =
- a = c â™
+ view first_pushout_view : frameworld:?OppositeLen/Solution -> ?SituationSpace/Derived1 =
+ include ?SituationSpace/Root/first_view â™
+ deducedLineCA = deducedLineCA â™
+ âš
+ view second_view : frameworld:?OppositeLen/Problem -> ?SituationSpace/Derived1 =
+ A = A â™
+ B = B â™
+ C = C â™
+ distanceBC = distanceBC â™
+ angleB = angleB â™
+ rightAngleC = rightAngleC â™
+ âš
âš
- âš
-âš
\ No newline at end of file
+âš
+
diff --git a/source/Scrolls/README.md b/source/Scrolls/README.md
index df4a964df9bde9872445f442af2398f69dd695ff..6c646c9e7f049390b4cd1cbd6f4cb9c195d789d3 100644
--- a/source/Scrolls/README.md
+++ b/source/Scrolls/README.md
@@ -9,58 +9,58 @@ Let us write a scroll "Midpoint" that requires two points `P` and `Q` as input,
```mmt
theory Midpoint =
- // A scroll is a theory with two special meta datums referencing a problem and a solution theory: â™
- meta ?MetaAnnotations?problemTheory ?Midpoint/Problem â™
- meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution â™
+ // A scroll is a theory with two special meta datums referencing a problem and a solution theory: â™
+ meta ?MetaAnnotations?problemTheory ?Midpoint/Problem â™
+ meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution â™
- // You can specify those theories as nested theories of the scroll theory as such, but this is not required at all; it is just convention. â™
+ // You can specify those theories as nested theories of the scroll theory as such, but this is not required at all; it is just convention. â™
- theory Problem =
- // Declare all required fact inputs here.
+ theory Problem =
+ // Declare all required fact inputs here.
- For every fact, you may (but are not required to) give some meta information
- like a label and description. â™
+ For every fact, you may (but are not required to) give some meta information
+ like a label and description. â™
- P
- : point â˜
- meta ?MetaAnnotations?label "P" â˜
- meta ?MetaAnnotations?description "Some arbitrary input point"
- â™
+ P
+ : point â˜
+ meta ?MetaAnnotations?label "P" â˜
+ meta ?MetaAnnotations?description "Some arbitrary input point"
+ â™
- Q
- : point â˜
- meta ?MetaAnnotations?label "Q" â˜
- meta ?MetaAnnotations?description "Some other arbitrary input point"
- â™
- âš
+ Q
+ : point â˜
+ meta ?MetaAnnotations?label "Q" â˜
+ meta ?MetaAnnotations?description "Some other arbitrary input point"
+ â™
+ âš
- theory Solution =
- // A solution theory always starts with including the problem theory: â™
- include ?Midpoint/Problem â™
+ theory Solution =
+ // A solution theory always starts with including the problem theory: â™
+ include ?Midpoint/Problem â™
- // Next, we can supply a label and a description to be used for the overall scroll:â™
- meta ?MetaAnnotations?label "MidPoint" â™
- meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." â™
+ // Next, we can supply a label and a description to be used for the overall scroll:â™
+ meta ?MetaAnnotations?label "MidPoint" â™
+ meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." â™
- // Here, the description uses MMT's interpolation feature by prefixing the double quotes with an "s".
- This allows embedding arbitrary MMT terms within the string via ${...} where ... is an MMT term.
+ // Here, the description uses MMT's interpolation feature by prefixing the double quotes with an "s".
+ This allows embedding arbitrary MMT terms within the string via ${...} where ... is an MMT term.
- In FrameIT, we use such string interpolation to give the scroll a more dynamic flavor:
-
- If the user fills the first P fact slot by a point with label A, then the scroll description should also talk about A, not P.
- For that we can use the MMT term `lverb P` that stands for "label verbalization" of P embedded into the description string via "${lverb P}".
- Whenever the user reassigns the fact slot for P, the label verbalization will kick in again and adjust the result of "${lverb P}" to the label of the actually assigned fact.
-
- And "${lverb P Q}" is syntactic sugar for "${lverb P}${lverb Q}", i.e., the mere concatenation (without whitespace). â™
+ In FrameIT, we use such string interpolation to give the scroll a more dynamic flavor:
+
+ If the user fills the first P fact slot by a point with label A, then the scroll description should also talk about A, not P.
+ For that we can use the MMT term `lverb P` that stands for "label verbalization" of P embedded into the description string via "${lverb P}".
+ Whenever the user reassigns the fact slot for P, the label verbalization will kick in again and adjust the result of "${lverb P}" to the label of the actually assigned fact.
+
+ And "${lverb P Q}" is syntactic sugar for "${lverb P}${lverb Q}", i.e., the mere concatenation (without whitespace). â™
- // Next, solution theories declare all facts that are acquired upon successful application: â™
+ // Next, solution theories declare all facts that are acquired upon successful application: â™
- midpoint
- : point â˜
- = ⟨0.5 â‹… (P _x + Q _x), 0.5 â‹… (P _y + Q _y), 0.5 â‹… (P _z + Q _z)⟩ â˜
- meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" â˜
- meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
- â™
- âš
+ midpoint
+ : point â˜
+ = ⟨0.5 â‹… (P _x + Q _x), 0.5 â‹… (P _y + Q _y), 0.5 â‹… (P _z + Q _z)⟩ â˜
+ meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" â˜
+ meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
+ â™
+ âš
âš
```