Proplogic / Fologic modules

Often describing problems in terms of states and actions may be a daunting task itself. Another approach to specifying the same comes from the area of Mathematical Logic. If you've taken a course in Logic Programming (especially if you are studying at FMI, SU) you are probably scared and willing to close this page ASAP but worry not since Adder make a great job at hiding all the hideous details of logic and you only need to care of the fun stuff.

Primer in Math Logic

Logic arose in Ancient Greece (due to Aristotle) but it was not before the famous English mathematician George Boole mixed it with math to produce a new science that later fathered the computer sciences. At large, logic defines an easy to understand special-purpose language which eases describing the world. There are many different type of logic, Adder currently implements 2 of them, more are coming soon.

Propositional logic

We'll start with the easiest of them all - propositional logic. Propositional logic consists of atomic statements (constants) and the Boolean functions (connectives) AND (&), OR (|), NOT (!), implication (=>) and equivalence (<=>). The meaning of the connectives should be obvious from their names so let's look at a few examples at how to translate English sentence to propositional:

English	Propositional logic
I am a smart and handsome man	I_am_smart & I_am_handsome
If my son is successful then I'll be a proud parent.	Son_is_successful => Proud_me
You can't have the cake and eat it too	Have_Cake <=> !Ate_Cake

Great, we can now express information in the propositional language. Next step would be to express all of our knowledge about the problem in the same way. The place where all that information is stored is called a knowledge base. Consider the following problem:

I am a hitchhiker travelling across the universe. Every hitchhiker must bring his own towel in order to be successful in his endeavors. Otherwise, the hitchhiker must put his life in the hands of one depressed paranoid robot. Must I bring with a towel with myself in order to be a successful hitchhiker if I can't afford a paranoid robot?

We can translate it in logic:

I_am_hitchhiker
I_am_hitchhiker => Hitchhiker
Hitchhiker & (Towel | Paranoid_Robot) <=> Success

The question is now: "In the above knowledge base, is the statement Towel & !Paranoid_Robot => Success true?"

There are algorithms that can solve that question and Adder provides them. Here's a snippet that solves the previous question:

from adder.proplogic import KnowledgeBase

kb = KnowledgeBase("""
    I_am_hitchhiker
    I_am_hitchhiker => Hitchhiker
    Hitchhiker & (Towel | Paranoid_Robot) <=> Success
""", 4, True)
print(kb.ask("Towel & !Paranoid_Robot => Success")) # True

That's all it takes. Just describe your knowledge base and start asking questions. You can run python main.py resolutionkb to test the example. If you need to add an additional sentence to the knowledge base, you can do so via the kb.tell method.

You've probably noticed the extra parameters on the KnowledgeBase constructor. They vastly improve the performance of the ask method. The first one is the maximum clause length - a magical number which you should set to the maximum number of elements that any statement has. In our example the last sentence has the most symbols - 4 (Hitchiker, Towel, Paranoid_Bot, Success). The second argument determines whether the knowledge base is complete. In a complete knowledge base either a statement is true or its negation is true. For most real world kbs this property holds so you can safely use True.

Unfortunately, the general algorithm for solving these kinds of question is kinda slow (exponential in the worst case). Adder also provides the adder.proplogic.DefiniteKnowledgeBase that solves queries in linear time but all the statements in the knowledge base must be either of the form A1 & A2 & A3 & ... & An => B (definite clauses) or of the form A (facts).

First-order logic

Propositional logic might be cool but certainly it isn't panacea. For instance, say that you have a knowledge base about a zoo shop with 5 animals. You'd like to assert that exactly at least of them is sick and needs to see the vet. You can do so like that:

Animal1_Sick | Animal2_Sick | Animal3_Sick | Animal4_Sick | Animal5_Sick

What if you had a 100 animals? Or perhaps a 1000 animals? Wouldn't it be great if there was a way to say that there exists a sick animal? Sure thing, Adder comes equipped with that too. Just use a first-order logic knowledge base! FO logic extends the propositional language by adding variables, functions, predicates and quantifiers.

Imagine we need to model a zoo shop which has 5 animals - Kitty the cat,, Doggy the dog, Bunny the rabbit, Linux the penguin and Evil, the mosquito. One of them is sick and needs to see the vet but we don't know which one. We only know that if an animal refuses to eat then it must be sick. In other words all animals that refuse to eat are sick. Finally, we know that Bunny refuses to eat. The previous paragraph translated in a FO knowledge base looks like this:

from adder.fologic import KnowledgeBase

kb = KnowledgeBase("""
    Animal(Kitty) & Animal(Doggy) & Animal(Bunny) & Animal(Linux) & Animal(Evil)
    E x(Animal(x) & Sick(x))
    V x(Animal(x) & RefusesToEat(x) => Sick(x))
    RefusesToEat(Bunny)
""", 4, True)
print(kb.ask("E x(Sick(x))")) # { "x": "Bunny" }

A quick overview of the above code:

• All objects must be PascalCased (as in Doggy, Bunny, Linux).
• To describe one object's properties we use predicates (Kitty is animal because we asserted that Animal(Kitty).
• All variables must be camelCased (as in x).
• Variables are introduced in either existential quantifiers (E x(...)) or universal quantifiers (V x(...)).
• An existential quantifier E x(P(x)) should be read as "There exists an object x for which the property P holds".
• Analogously, V x(P(x)) means "For all objects the property P holds".

That's all you need to know to start designing your own knowledge bases. The additional arguments passed to the KnowledgeBase constructor stand for the same thing as in the propositional case.

Once again, the general algorithm is rather slow and Adder provides an alternative for the definite case - adder.fologic.DefiniteKnowledgeBase. Sentences in the latter may not contain existential quantifiers and all universal quantifiers are implicit. Instead of V x(Animal(x) & RefusesToEat(x) => Sick(x)) you should use Animal(x) & RefusesToEat(x) => Sick(x).

That's all folks! Make sure to mail me for any additional questions.