This project’s GitHub page: https://github.com/SSODelta/LoGiX

LoGiX is a program for determining if a certain boolean expression is a semantic consequence of some list of premises.

Posts about LoGiX

LoGiX – An Overview

For the past week or so, I’ve been working on a program I call LoGiX. In it’s essense, it can be used to verify the validity of logical arguments based on a list of accepted premises. This means for instance that we can solve logical puzzles, such as the ones on http://4chests.blogspot.dk/.

Syntax

As of now, we don’t need to introduce all the commands of LoGiX, but let’s look at two simple commands:

def [EXPRESSION] [EXPRESSION]?

Writing def defines a premise – an expression assumed true. Writing an expression followed by a question mark will ask LoGiX to verify whether or not the expression in question is a semantic consequence of the premises.

To make a really simple example demonstrating LoGiX, let , , and be three propositions. Then define that . Then we can ask LoGiX if is a semantic consequence based on our premises (as would be expected). Written in LoGiX, we get:

def P or Q implies R P implies R?

For which the output is “true”.

A more complicated example

To really show the power of LoGiX, let’s quickly go over a more complicated example:

Determine who out of the following is guilty of doping. The suspects are: Sam, Michael, Bill, Richard, Matt. 1) Sam said: Michael or Bill took drugs, but not both. 2) Michael said: Richard or Sam took drugs, but not both. 3) Bill said: Matt or Michael took drugs, but not both. 4) Richard said: Bill or Matt took drugs, but not both. 5) Matt said: Bill or Richard took drugs, but not both. 6) Tom said: If Richard took drugs, then Bill took drugs. Statement 6 is guaranteed to be true, and 4 out of statements 1-5 are false.

We’re going to model this logical puzzle in LoGiX and determine which of the suspects are guilty of doping. Let’s ignore the last line as of now, and only focus on statements 1-6, which gives:

TrueSam biimplies MichaelDrug xor BillDrug TrueMichael biimplies RichardDrug xor SamDrug TrueBill biimplies MattDrug xor MichaelDrug TrueRichard biimplies BillDrug xor MattDrug TrueMatt biimplies BillDrug xor RichardDrug RichardDrug implies BillDrug

Looking at the first line, we see that if Sam is speaking the truth (TrueSam) then Michael took drugs (MichaelDrug) or Bill took drugs (BillDrug), but no both (hence the XOR) – notice that this is a bi-implication. Likewise, the last line says that if Richard took drugs (RichardDrug) then Bill took drugs (BillDrug), which is not a bi-implication.

We also need to model the statement that says that 4 of statements 1-5 are false. Note that this is analogous to saying the exactly one of Sam, Michael, Bill, Richard and Matt are speaking the truth. We can model this in LoGiX as:

exactly 1 of TrueSam, TrueMichael, TrueBill, TrueRichard, TrueMatt

Since we’re trying to find the person taking drugs, we are, in fact, also implying that only one person took drugs. Therefore, we also need to write:

exactly 1 of SamDrug, MichaelDrug, BillDrug, RichardDrug, TrueMatt

Since we’ve now modelled the entire puzzle in LoGiX, we can ask:

MichaelDrug? BillDrug? SamDrug? MattDrug? RichardDrug?

Which returns true only for SamDrug implying that Sam is the perpetrator.

Additional features

In some puzzles, we’re being told that a minimum of some propositions are true. Therefore we can write:

minimum [NUMBER] of [EXPRESSION_LIST]

Which defines that at least [NUMBER] of the list of expressions are true. Likewise we can define:

maximum [NUMBER] of [EXPRESSION_LIST]

I’ve found that one of the hardest things to do is actually interpreting the puzzles, so when you’re not getting the results you want, it’s possible to find an example of some expression having some value to try to find a contradiction. I’ve done this often when trying to debug my LoGiX programs, so I made a command in LoGiX. Which means you can write:

example [FALSE/TRUE] [EXPRESSION]

To get an example of the values of the boolean variables, when [EXPRESSION] is [FALSE/TRUE].

Likewise, if we want to know in how many cases an expression is true, we can use the following function:

num [EXPRESSION]

Which returns two numbers (e.g. 7/8) which denotes in how many cases the expression is true.

Comments and Printing

Any line prepended with pound-sign # will be ignored by the LoGiX-compiler which makes it easy to make comments:

#This line will be ignored by LoGiX This line will not (and gives an error)

Also, LoGiX will print the output of any line when reading a file. Which means that we’ll get the following output from this file (output is prepended by > in this example):

P or Q implies R >def P or Q implies R P implies R? >true

This can get messy really quickly when writing more complicated LoGiX programs, so it’s possible to designate when you want LoGiX to print its output. Writing !! toggles the global printing, and prepending a line with ! toggles printing for that specific line. This means that the following program:

!! P or Q implies R !P implies R?

Will only print true as its output.

Custom messages

It may be of benefit sometimes to have LoGiX write other output when some statement turns out to be true. Therefore, any message appended after ? when testing the validity of an expression will be printed instead of true if that expression turns out to be a semantic consequence of our premises. This means that:

!! P or Q implies R !P implies R?Yup, P implies R!

Will print “Yup, P implies R!”. We can also specify custom messages for when an expression is false. Anything after | will be interpreted as the custom message for when the expression is not a semantic consequence of our premises. Therefore, the following program:

!! P or Q implies R !R implies P?|They're not equal.

Prints only “They’re not equal“.

Relations and Types

For more complex situations, you may need to specify relations between certain objects. First of all, let’s learn how to define a type.

obj TYPE_NAME OBJ_1, OBJ_2, ... OBJ_N

Which defines a type with the name TYPE_NAME, and states that this type contains the objects OBJ_1, OBJ_2 … OBJ_N. As an example, let’s define a type:

obj Person Mark, John, Richie

So, we’ve defined a type – a person – and its contents are Mark, John and Richie. It’s important to note that both the type name and the objects in it have to start with a capital letter, and that none of them can share a name.

To define a relation, we do the following:

rel RELATION_NAME(TYPE_1, TYPE_2, ... TYPE_N)

Which defines an n-ary relation between the types within the parentheses. As an example, let’s define a simple relation using the above type:

rel IsFriendWith(Person, Person)

Which enables us to say that any two people are friends. Therefore, we could define:

def IsFriendWith(Mark, John)

Which states that Mark is friends with John. Commen sense tells us that this should also imply that John is friends with Mark (one-sided friendships might exists, but not in this example). But as it gets tedious to write all the relations, we can define general procedures about relations. For instance, the friend relation is reflexive which means that we can write:

def IsFriendWith(x,y) implies IsFriendWith(y,x)

Which says that if some person x is friends with some other person y, then y is also friends with x. Note that x and y are placeholder variables here. In this concrete example, we wouldn’t have needed to specify the above line. We could have written a modifier when defining the relation in the first place:

rel REF IsFriendsWith(Person, Person)

Which tells LoGiX that the relation is reflexive. Likewise, we can use any of the following modifiers:

REF – Reflexive

STRICT – Irreflexive, Strict

SYM – Symmetric

ASYM – Asymmetric

TOTAL – Total

TRANS – Transitive

EUCLIDEAN – Euclidean

EQ – Equality (Reflexive + Symmetric + Transitive)

Note that these modifiers only work when we’re dealing with binary relations of the same type. For instance, this program does not make any sense:

obj House NiceHouse, DecentHouse, PoorHouse obj Person Mark, John, Richie rel REF LivesIn(Person, House) def LivesIn(Mark, NiceHouse)

Because this implies that NiceHouse lives in Mark, which contextually doesn’t make any sense.

A really complicated example (Lewis Carroll)

Let’s take a look at the following riddle by author Lewis Carroll:

All the dated letters in this room are written on blue paper. None of them are in black ink, except those that are written in the third person. I have not filed any of those that I can read. None of those that are written on one sheet are undated. All of those that are not crossed out are in black ink. All of those that are written by Brown begin with “Dear Sir.”. All of those that are written on blue paper are filed. None of those that are written on more than one sheet are crossed out. None of those that begin with “Dear sir” are written in the third person. Therefore, I cannot read any of Brown’s letters.

I love this riddle because it elegantly shows how limited the human brain is – I can’t follow Lewis Carroll’s argument. It doesn’t make any sense to me that he cannot read any of Brown’s letter based on this argument, but LoGiX can tell you. Based on this argument, we can come up with the following LoGiX code:

!! #All the dated letters in this room are written on blue paper. if DatedLetter then BluePaper #None of them are in black ink, except those that are written in the third person. if not ThirdPerson then not BlackInk #I have not filed any of those that I can read. if CanRead then not Filed #None of those that are written on one sheet are undated. if OneSheet then DatedLetter #All of those that are not crossed out are in black ink. if not Crossed then BlackInk #All of those that are written by Brown begin with "Dear Sir." if Brown then DearSir #All of those that are written on blue paper are filed. if BluePaper then Filed #None of those that are written on more than one sheet are crossed out. if not OneSheet then not Crossed #None of those that begin with "Dear sir" are written in the third person. if DearSir then not ThirdPerson #So, I can't read Brown's letters? !Brown implies not CanRead

Which returns true, proving that Lewis Carroll is a genius.