interval characterization proofs and worked examples

1 files changed, 27 insertions, 0 deletions

diff --git a/examples/family.sol b/examples/family.sol
new file mode 100644
index 0000000..8d1f7f9
--- /dev/null
+++ b/examples/family.sol
@@ -0,0 +1,27 @@
+% Relations, facts, rules, joins and negation.
+
+Relation named: Person schema: #(
+  [name domain: String]
+  [age domain: Integer]
+)
+
+[Person name: "Marcos" age: 30]
+[Person name: "Ana" age: 12]
+[Person name: "Rui" age: 70]
+
+Rule name: "an adult is a person of age at least 18"
+     head: [Adult name: N]
+     body: [Person name: N age: A] :and
+           [GreaterEqual left: A right: 18]
+
+% Everyone stored.
+Query expression: [Person name: N age: A]
+
+% The rule, joined through the shared variable N.
+Query expression: [Adult name: N]
+
+% Decidable denial: people who are not adults.
+Query expression: ([Person name: N age: A]) :not [Adult name: N]
+
+% The specification's negation form, scoped by the universe.
+Query expression: [World] :not [Adult name: "Ana"]