commit
1816741ce6
21 changed files with 194 additions and 1 deletions
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
@ -1 +1 @@ |
||||
Subproject commit 9a10b5a2676264aa47f6a29db03f46e4922a2862 |
||||
Subproject commit 6584acab72f449c3f8ccd0f8772df9e5266bc830 |
Binary file not shown.
@ -0,0 +1,68 @@ |
||||
/** |
||||
* A Database as a logical structure |
||||
*/ |
||||
vocabulary Sigma { |
||||
/* |
||||
* The assignment uses untyped first order logic. This is why we use a type "object" representing all object in the domain. |
||||
* In real applications, we would make types like person, instructor, student, course etc. |
||||
* It is a good idea to try this. |
||||
* |
||||
* constructed from already includes UNA and DCA!!!!!! |
||||
*/ |
||||
type domain constructed from { A, AA, AAA, Ann, B, Bill, C, CS148, CS230, CS238, D, F, Flo, Hec, Jack, Jill, M100, M200, May, Pat, Ray, Sam, Sue, Tom } |
||||
|
||||
Instructor(domain, domain) |
||||
Prerequ(domain, domain) |
||||
Enrolled(domain, domain) |
||||
Grade(domain, domain, domain) |
||||
PassGrade(domain) |
||||
} |
||||
|
||||
structure Database : Sigma { |
||||
Instructor = { |
||||
Ray(), CS230(); |
||||
Hec(), CS230(); |
||||
Sue(), M100(); |
||||
Sue(), M200(); |
||||
Pat(), CS238(); |
||||
} |
||||
Prerequ = { |
||||
CS230(), CS238(); |
||||
CS148(), CS230(); |
||||
M100(), M200(); |
||||
} |
||||
Enrolled = { |
||||
Jill(), CS230(); |
||||
Jack(), CS230(); |
||||
Sam(), CS230(); |
||||
Bill(), CS230(); |
||||
May(), CS238(); |
||||
Ann(), CS238(); |
||||
Tom(), M100(); |
||||
Ann(), M100(); |
||||
Jill(), M200(); |
||||
Sam(), M200(); |
||||
Flo(), M200(); |
||||
} |
||||
Grade = { |
||||
Sam(), CS148(), AAA(); |
||||
Bill(), CS148(), D(); |
||||
Jill(), CS148(), A(); |
||||
Jack(), CS148(), C(); |
||||
Flo(), CS230(), AA(); |
||||
May(), CS230(), AA(); |
||||
Bill(), CS230(), F(); |
||||
Ann(), CS230(), C(); |
||||
Jill(), M100(), B(); |
||||
Sam(), M100(), AA(); |
||||
Flo(), M100(), D(); |
||||
Flo(), M100(), B() |
||||
} |
||||
PassGrade = { |
||||
AAA(); |
||||
AA(); |
||||
A(); |
||||
B(); |
||||
C(); |
||||
} |
||||
} |
@ -0,0 +1,40 @@ |
||||
include "database.idp" |
||||
include "run_queries.idp" |
||||
|
||||
procedure main() { |
||||
queries = {O1Q1;O1Q2;O1Q3;O1Q4;O1Q5;O1Q6;O1Q7} |
||||
runTrueFalseQueries(queries) |
||||
} |
||||
|
||||
/* |
||||
* TODO: complete the queries. Since these are true/false queries, nothing should be added in front of the colon |
||||
* (there are no variables) |
||||
* replace true or false by the relevant formula (the values as they are given are insignificatn) |
||||
*/ |
||||
query O1Q1: Sigma { |
||||
{ : ?x: Prerequ(x, CS238) } |
||||
} |
||||
|
||||
query O1Q2: Sigma { |
||||
{ : ?x: Grade(May, CS230, x) & PassGrade(x) } |
||||
} |
||||
|
||||
query O1Q3: Sigma { |
||||
{ : !x: Prerequ(x, M100) => Instructor(Ray, x) } |
||||
} |
||||
|
||||
query O1Q4: Sigma { |
||||
{ : !x: Enrolled(x, CS230) => ?g: Grade(x, CS230, g) & PassGrade(g)} |
||||
} |
||||
|
||||
query O1Q5: Sigma { |
||||
{ : /*?g: Grade(John, CS230, g)*/ false} |
||||
} |
||||
|
||||
query O1Q6: Sigma { |
||||
{ : ?s: !i: ?c: Enrolled(s, c) & Instructor(i, c)} |
||||
} |
||||
|
||||
query O1Q7: Sigma { |
||||
{ : ?s: ?1c: Enrolled(s, c) } |
||||
} |
@ -0,0 +1,21 @@ |
||||
include "database.idp" |
||||
include "run_queries.idp" |
||||
|
||||
procedure main() { |
||||
queries = {O2Q1;O2Q2;O2Q3} |
||||
displayQueryAnswers(queries) |
||||
} |
||||
|
||||
// TODO: complete queries. |
||||
|
||||
query O2Q1: Sigma{ |
||||
{s[domain] c[domain] : ?g: Grade(s, c, g) & PassGrade(g)} |
||||
} |
||||
|
||||
query O2Q2: Sigma{ |
||||
{s[domain] : ?1c: Enrolled(s, c)} |
||||
} |
||||
|
||||
query O2Q3: Sigma{ |
||||
{s[domain] : Enrolled(s, CS230) & !c: !g: Grade(s, c, g) => PassGrade(g)} |
||||
} |
@ -0,0 +1,29 @@ |
||||
include "database.idp" |
||||
include "run_queries.idp" |
||||
|
||||
procedure main() { |
||||
integrityConstraints = {IntegrityConstraint1,IntegrityConstraint2,IntegrityConstraint3,IntegrityConstraint4} |
||||
|
||||
allIntegrityConstraints = merge(IntegrityConstraint1,IntegrityConstraint2) |
||||
allIntegrityConstraints = merge(allIntegrityConstraints,IntegrityConstraint3) |
||||
allIntegrityConstraints = merge(allIntegrityConstraints,IntegrityConstraint4) |
||||
// This way, you can combine all the integrityConstraints to One big theory representing integrity of the database. |
||||
|
||||
testIntegrityConstraints(integrityConstraints) |
||||
} |
||||
|
||||
// TODO: add integrity constraints |
||||
|
||||
theory IntegrityConstraint1 : Sigma { |
||||
false. |
||||
} |
||||
|
||||
theory IntegrityConstraint2 : Sigma { |
||||
false. |
||||
} |
||||
theory IntegrityConstraint3 : Sigma { |
||||
false. |
||||
} |
||||
theory IntegrityConstraint4 : Sigma { |
||||
false. |
||||
} |
@ -0,0 +1,35 @@ |
||||
include <table_utils> |
||||
|
||||
procedure runTrueFalseQueries(queries) { |
||||
for index = 1, #queries do |
||||
result = query(queries[index], Database) |
||||
print("Query "..index.." evaluates to ", result) |
||||
end |
||||
} |
||||
|
||||
procedure displayQueryAnswers(queries) { |
||||
for index = 1, #queries do |
||||
print("Running query "..index) |
||||
result = query(queries[index], Database) |
||||
|
||||
print("Result is:") |
||||
print(result) |
||||
end |
||||
} |
||||
|
||||
procedure testIntegrityConstraints(constraints) { |
||||
// We assume that database is two-valued. Hence: all we should check is: is database a model of every constraint. |
||||
|
||||
for index = 1, #constraints do |
||||
print("Testing constraint "..index) |
||||
stdoptions.nbmodels = 1 |
||||
result = (#modelexpand(constraints[index], Database) > 0) |
||||
// Alternatively to using the sat-inferences, we could use modelexpand and check if the result has at least one model |
||||
// (in our case: exactly one model) |
||||
if result then |
||||
print("Database satisfies constraint "..index) |
||||
else |
||||
print("Database does not satisfy constraint "..index) |
||||
end |
||||
end |
||||
} |
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Loading…
Reference in new issue