Logicals, which are logic routines, and represent logic programming, state the routine as a set of logical relations (e.g., a grandparent is the parent of a parent of someone). Such rutines are similar to the database languages. A program is executed by an “inference engine” that answers a query by searching these relations systematically to make inferences that will answer a query.
One of the main goals of the development of symbolic logic hasbeen to capture the notion of logical consequence with formal, mechanical, means. If the conditions for a certain class of problems can be formalized within a suitable logic as a set of premises, and if a problem to be solved can bestated as a sentence in the logic, then a solution might be found by constructing a formal proof of the problem statement from the premises
Declaration
In FOL, logic programming is considered as a first class citzen with axioms (axi) as facts and logicals (log) as rules, thus resembling Prolog language. For example:
Facts
Declaring a list of facts (axioms)
var likes: axi[str, str] = { {"bob","alice"} , {"alice","bob"}, {"dan","sally"} };
Rules
Declaring a rule that states if A likes B and B likes A, they are dating
log dating(a, b: str): bol = {
likes:[a,b] and
likes:[b,a]
}
Declaring a rule that states if A likes B and B likes A, they are just friends
log frends(a, b): bol = {
likes:[a,b] or
likes:[b,a]
}
Rules can have only facts and varibles within
Return
A logical log can return different values, but they are either of type bol, or of type container (axioms axi or vectors vec):
Lets define a axiom of parents and childrens called parents and another one of parents that can dance called dances:
var parent: axi[str, str] = { {"albert","bob"},
{"albert","betty"},
{"albert","bill"},
{"alice","bob"},
{"alice","betty"},
{"alice","bill"},
{"bob","carl"},
{"bob","tom"} };
var dances axi[str] = { "albert", "alice", "carl" };
Boolean
Here we return a boolean bol. This rule check if a parent can dance:
log can_parent_dance(a: str): bol = {
parent:[a,_] and dances:[a]
}
can_parent_dance("albert") // return true, "albert" is both a parent and can dance
can_parent_dance("bob") // return false, "bob" is a parent but can't dance
can_parent_dance("carl") // return false, "carl" is not a parent
Lets examine this:
parent:[a,_] and dances:[a]
this is a combintion of two facts. Here we say if a is parent of anyone (we dont care whose, that’s why we use meh symbol [a,_]) and if true, then we check if parent a (since he is a parent now, we fact-checked) can dance.
Vector
The same, we can create a vector of elements. For example, if we want to get the list of parents that dance:
log all_parents_that_dance(): vec[str] = {
parent:[*->X,_] and
dances:[X->Y]
Y
}
all_parents_that_dance() // this will return a string vector {"albert", "alice"}
Now lets analyze the body of the rule:
parent:[*->X,_] and
dances:[X->Y]
Y
Here are a combination of facts and variable assignment through silents. Silents are a single letter identifiers. If a silent constant is not declared, it gets declared and assigned in-place.
Taking a look each line:
parent:[X,_] and
this gets all parents ([*->X,_]),and assign them to silent X. So, X is a list of all parents.
then:
dances[X->Y]:
this takes the list of parents X and checks each if they can dance, and filter it by assigning it to Y so [X->Y] it will have only the parents that can dance.
then:
Y
this just returns the list Y of parents that can dance.
Relationship
If A is object and objects can be destroyed, then A can be destroyed. As a result axioms can be related or conditioned to other axioms too, much like facts.
For example: if carl is the son of bob and bob is the son of albert then carl must be the grandson of albert:
log grandparent(a: str): vec[str] = {
parent[*->X,a]: and
parent[*->Y,X]:
Y
}
Or: if bob is the son of albert and betty is the doughter of albert, then bob and betty must be syblings:
log are_syblings(a, b: str): vec[str] = {
parent[*->X,a]: and
parent[X->Y,b]:
Y
}
Same with uncle relationship:
var brothers: axi[str] = { {"bob":"bill"}, {"bill","bob"} };
log has_uncle(a: str): vec[str] = {
parent[*->Y,a]: and
brothers[Y,*->Z]:;
Z
}
Conditional facts
Here an example, the axioms hates will add a memeber romeo only if the relation x is satisfied:
var stabs: axi = {{"tybalt","mercutio","sword"}}
var hates: axi;
log romeHates(X: str): bol = {
stabs[X,"mercutio",_]:
}
hates+["romeo",X] if (romeHates(X));
Anonymous logicals
Conditional facts can be added with the help of anonymous logicals/rules:
eats+[x,"cheesburger"] if (eats[x,"bread"] and eats[X,"cheese"]);
eats+[x:"cheesburger"] if (log (a: str): bol = {
eats[a,"bread"]: and
eats[a,"cheese"]:
}(x));
Nested facts
var line: axi = { {{4,5},{4,8}}, {{8,5},{4,5}} }
log vertical(line: axi): bol = {
line[*->A,*->B]: and
A[*->X,Y*->]: and
B[X,*->Y2]:
}
log horizontal(line: axi): bol = {
line[*->A,*->B]: and
A[*->X,*->Y]: and
B[*->X2,Y]:
}
assert(vertical(line.at(0))
assert(horizontal(line.at(1))
Filtering
Another example of filtering a more complex axion:
var class: axi;
class.add({"cs340","spring",{"tue","thur"},{12,13},"john","coor_5"})
class.add({"cs340",winter,{"wed","fri"},{15,16},"bruce","coor_3"})
log instructor(class: str): vec[str] = {
class[class,_,[_,"fri"],_,*->X,_]
X
}