The Knowledge Base

This is the knowledge base formed by merging the contributions from our four volunteers.

A description of the predicates and variable types can be found here.

Misc
TaughtBy(C, P, Q) ^ CourseLevel(C, level_500) => Professor(P)
TaughtBy(C, P, Q) ^ Student(P) => !CourseLevel(C, level_500)
TaughtBy(C, P, Q) ^ Student(P) => !Phase(P, pre_Quals)
TaughtBy(C, P, Q) ^ Student(P) => !YearsInProgram(P, year_1)
TempAdvisedBy(P, S) => Professor(P)
TempAdvisedBy(P, S) => Student(S)
TempAdvisedBy(P, S) => Position(P, faculty)
TempAdvisedBy(P, S) => Phase(S, pre_Quals)
TempAdvisedBy(P, S) => YearsInProgram(P, year_1) or YearsInProgram(P, year_2)
TA(C, P, Q) => Student(P)
TaughtBy(C, P, Q) ^ CourseLevel(C, level_500) ^ TA(C, S, Q) => AdvisedBy(S, P) or TempAdvisedBy(S,P)
AdvisedBy(P, S) => Student(S)
AdvisedBy(P, S) => Professor(P)
AdvisedBy(P, S) => !YearsInProgram(P, year_1)
Publication(P, X) ^ Publication(P,Y) ^ Student(X) ^ !Student(Y) => Professor(Y)
Publication(P, X) ^ Publication(P,Y) ^ Student(X) ^ !Student(Y) => AdvisedBy(X,Y) or TempAdvisedBy(X,Y)
Student(X) => !Professor(X)
Professor(X) => !Student(Y)
Student(X) => AdvisedBy(X,Y) or TempAdvisedBy(X,Y)
Professor(P) ^ Position(P, faculty) => TaughtBy(C, P, Q)
Phase(S, post_Quals) => !YearsInProgram(year_1)
Phase(S, pre_Quals) => !Phase(S, post_Quals)
Phase(S, pre_Quals) => !Phase(S, post_Generals)
Phase(S, post_Quals) => !Phase(S, pre_Quals)
Phase(S, post_Quals) => !Phase(S, post_Generals)
Phase(S, post_Generals) => !Phase(S, pre_Quals)
Phase(S, post_Generals) => !Phase(S, post_Quals)
Professor(P) => Position(P, faculty) or Position(P, faculty_affiliate) or Position(P, faculty_adjunct) or Position(P, faculty_emeritus) or Position(P, faculty_visiting)
Position(P, faculty_visiting) => !AdvisedBy(S, P)
originally written by volunteer as Position(P, faculty_visiting) => !(exists S, AdvisedBy(S,P)
Professor(X) ^ Position(X, faculty) => AdvisedBy(S,X) or TempAdvisedBy(S,X)
Student(P) ^ !YearsInProgram(year_1) => TA(C, P, Q)
Advisement
AdvisedBy(X,Y) => Student(X)
AdvisedBy(X,Y) => Professor(Y)
TempAdvisedBy(X,Y) => Student(X)
TempAdvisedBy(X,Y) => Professor(Y)
Position(X,T) => Professor(X)
TempAdvisedBy(X,Y) => !Position(X,faculty_visiting)
TempAdvisedBy(X,Y) ^ !YearsInProgram(X,year_1) => YearsInProgram(X,year_2)
TempAdvisedBy(X,Y) => Phase(X,pre_Quals)
Exists Y: Student(X) ^ !AdvisedBy(X,Y) => TempAdvisedBy(X,Y)
Exists Y: Professor(X) ^ !Position(X, faculty_visiting) => AdvisedBy(Y,X)
Misc
TaughtBy(C,X,Q) => Professor(X)
TA(C,X,Q) => Student(X)
Phases and positions
Phase(X,Y) => Student(X)
Student(X) => Phase(X,pre_Quals) or Phase(X,post_Quals) or Phase(X,post_Generals)
Phase(X,pre_Quals) => !Phase(X,post_Quals)
Phase(X,post_Quals) => !Phase(X,pre_Quals)
Phase(X,post_Generals) => !Phase(X,post_Quals)
Position(X,Y) ^ Position(X,Z) => SamePosition(Y,Z)
Exists P: Phase(X, post_Generals) => Publication(P,X)
Exists Y: Professor(X) => Position(X,Y)
Predicate constraints
!AdvisedBy(A,A)
!TempAdvisedBy(A,A)
AdvisedBy(A,B) => !AdvisedBy(B,A)
TempAdvisedBy(A,B) => !TempAdvisedBy(B,A)
AdvisedBy(S:Person, P:Person) ^ !SamePerson(P,Q) => !AdvisedBy(S:Person, Q:Person)
TempAdvisedBy(S:Person, P:Person) ^ !SamePerson(P,Q) => !TempAdvisedBy(S:Person, Q:Person)
AdvisedBy(S:Person, P:Person) => !TempAdvisedBy(S:Person, Q:Person)
TempAdvisedBy(S:Person, P:Person) => !AdvisedBy(S:Person, Q:Person)
Phase
Phase(S,pre_Quals) => !AdvisedBy(S,P)
Phase(S,post_Quals) => !TempAdvisedBy(S,P)
Phase(S,post_Generals) => !TempAdvisedBy(S,P)
Teaching and AdvisedBy
Exists Y: TaughtBy(C,X,Q) => TA(C,Y,Q)
Exists Y: TA(C,X,Q) => TaughtBy(C,Y,Q)
Phase(S,post_Quals) ^ TaughtBy(C,P,Q) ^ TA(C,S,Q) ^ !CourseLevel(C,level_100) => AdvisedBy(S,P)
Phase(S,post_Quals) ^ TaughtBy(C,P,Q) ^ !TA(C,S,Q) ^ !CourseLevel(C,level_100) => !AdvisedBy(S,P)
Phase(S,post_Quals) ^ !TaughtBy(C,P,Q) ^ TA(C,S,Q) ^ !CourseLevel(C,level_100) => !AdvisedBy(S,P)
Phase(S,post_Generals) ^ TaughtBy(C,P,Q) ^ TA(C,S,Q) ^ !CourseLevel(C,level_100) => AdvisedBy(S,P)
Phase(S,post_Generals) ^ TaughtBy(C,P,Q) ^ !TA(C,S,Q) ^ !CourseLevel(C,level_100) => !AdvisedBy(S,P)
Phase(S,post_Generals) ^ !TaughtBy(C,P,Q) ^ TA(C,S,Q) ^ !CourseLevel(C,level_100) => !AdvisedBy(S,P)
Publication and AdvisedBy
Publication(T:Title,A:Person) ^ Publication(T,B) ^ !SamePerson(A,B) => AdvisedBy(A,B) or AdvisedBy(B,A)
Publication(T,A) ^ Publication(T,B) ^ !SamePerson(A,B) ^ Professor(A) ^ Student(B) => AdvisedBy(B,A)
AdvisedBy(S,P) ^ Publication(T,S) => Publication(T,P)
Classes of people
TaughtBy(C:Course, P:Person, Q:Quarter) => Professor(P:Person)
Position(P:Person, X:Position) => Professor(P:Person)
AdvisedBy(S:Person, P:Person) => Student(S:Person)
AdvisedBy(S:Person, P:Person) => Professor(P:Person)
Phase(P:Person, X:Phase) => Student(P:Person)
TempAdvisedBy(S:Person, P:Person) => Student(S:Person)
TempAdvisedBy(S:Person, P:Person) => Professor(P:Person)
YearsInProgram(P:Person, X:Integer) => Student(P:Person)
TA(C:Course, P:Person, Q:Quarter) => Student(P:Person)
People belong to one class
!Student(P:Person) => Professor(P:Person)
Student(P:Person) => !Professor(P:Person)
Uniqueness constraints
Position(P:Person, X:Position) ^ !SamePosition(X,Y) => !Position(P:Person, Y:Position)
Phase(P:Person, X:Phase) ^ !SamePhase(X,Y) => !Phase(P:Person, Y:Phase)
YearsInProgram(P:Person, X:Integer) ^ !SameInteger(X,Y) => !YearsInProgram(P:Person, Y:Integer)
Generally true uniqueness constraints
TaughtBy(X:Course, P:Person, Q:Quarter) ^ !SameCourse(X,Y) => !TaughtBy(Y:Course, P:Person, Q:Quarter)
TaughtBy(C:Course, X:Person, Q:Quarter) ^ !SamePerson(X,Y) => !TaughtBy(C:Course, Y:Person, Q:Quarter)
TA(X:Course, P:Person, Q:Quarter) ^ !SameCourse(X,Y) => !TA(Y:Course, P:Person, Q:Quarter)
TA(C:Course, X:Person, Q:Quarter) ^ !SamePerson(X,Y) => !TA(C:Course, Y:Person, Q:Quarter)