Implementing a theorem prover in Scala.
[EDIT]
For those of you who are interested, I'll be putting here any interesting links I find during my endeavor.
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Cool MIT lecture notes on propositional and first
order logic automation (see chapters 9 and 10):
http://tinyurl.com/77nfyx9
Logic for Computer Science : Foundations
of Automatic Theorem Proving (free pdf)
http://www.cis.upenn.edu/~jean/gbooks/logic.html
On integrating theorem proving and symbolic computation...
http://www.calculemus.net/
http://tinyurl.com/7o99oot
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[/EDIT]
For the last couple of months, my duties have entailed helping a professor of mine discover new, interesting theorems in the domain of control theory. Whenever he comes up with something, I write a small Mathematica script to test its validity extensively, and if everything is OK, we proceed to trying to prove it. So far, we have some good results, but nothing too serious as to make us (rich and) famous overnight. So, one day I thought "OK, this is stupid. It's not going to get us anywhere good anytime soon. So, why don't we just automate the whole procedure?". And that's what I decided to do. I told him about my plan, but he didn't seem very enthusiastic, probably because he isn't much of a programmer himself. Nevertheless, I decided to proceed.
I googled a bit around "automated theorem proving" and got some good links. I did some studying on logic and stuff, and, eventually, my first attempt came to life. It's a propositional logic theorem prover. You give it a propositional formula, and it tells you if it's valid (always true), unsatisfiable (always false) or satisfiable (can be true). The first version was written in Haskell. However, I realized that there are two problems with this approach. The first one is that this algorithm doesn't work for every kind of logic. It only works with propositional and first-order logic. And I want more. The higher the order of the logic I use, the more detailed the modeling of my domain can be and, therefore, the more interesting the theorems I can describe and prove can be. The second problem is that I want not only a theorem prover, but also a theorem generator. I'd like to have something that I feed with all sorts of axioms and spits out all sorts of interesting theorems deriving from these axioms. To deal with these problems, it looks like I'll have to use stuff like pathfinding algorithms with smart heuristics. Now, I seriously doubt my ability to code something like A* in Haskell, in a way that is both simple and efficient, so, I decided to switch to Scala, where I can mix imperative and functional style any way I want.
Ok, that was enough introduction. Here's the code -> http://ideone.com/P2deE
I'd really appreciate it if a (certain) Scala specialist could review the code and tell me how I could make it smaller and / or faster. The code is an almost direct translation of the Haskell version, so, I think there are parts that would be better written in imperative style. For example, I believe the lcnf function could make use of list buffers. Also, about that same function, I tried to implement it like this...
...but it didn't work :/ It seems that I can't pattern match against T. Why? Is there a workaround?
Has anyone else played with stuff like that? If yes, do you have any good (preferably online) studying material I could use?
Finally, if you want, you can help me submit it bug-free to daniweb's code snippet competition. Just try any crazy propositional formula you can think of and tell me if you get a wrong result. I think you can actually do it on the same ideone paste I posted above.
EDIT: Fixed two bugs that caused it to enter an infinite loop for some inputs.
EDIT2: Another bug fix... It should be ok now... I guess...
For those of you who are interested, I'll be putting here any interesting links I find during my endeavor.
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Cool MIT lecture notes on propositional and first
order logic automation (see chapters 9 and 10):
http://tinyurl.com/77nfyx9
Logic for Computer Science : Foundations
of Automatic Theorem Proving (free pdf)
http://www.cis.upenn.edu/~jean/gbooks/logic.html
On integrating theorem proving and symbolic computation...
http://www.calculemus.net/
http://tinyurl.com/7o99oot
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[/EDIT]
For the last couple of months, my duties have entailed helping a professor of mine discover new, interesting theorems in the domain of control theory. Whenever he comes up with something, I write a small Mathematica script to test its validity extensively, and if everything is OK, we proceed to trying to prove it. So far, we have some good results, but nothing too serious as to make us (rich and) famous overnight. So, one day I thought "OK, this is stupid. It's not going to get us anywhere good anytime soon. So, why don't we just automate the whole procedure?". And that's what I decided to do. I told him about my plan, but he didn't seem very enthusiastic, probably because he isn't much of a programmer himself. Nevertheless, I decided to proceed.
I googled a bit around "automated theorem proving" and got some good links. I did some studying on logic and stuff, and, eventually, my first attempt came to life. It's a propositional logic theorem prover. You give it a propositional formula, and it tells you if it's valid (always true), unsatisfiable (always false) or satisfiable (can be true). The first version was written in Haskell. However, I realized that there are two problems with this approach. The first one is that this algorithm doesn't work for every kind of logic. It only works with propositional and first-order logic. And I want more. The higher the order of the logic I use, the more detailed the modeling of my domain can be and, therefore, the more interesting the theorems I can describe and prove can be. The second problem is that I want not only a theorem prover, but also a theorem generator. I'd like to have something that I feed with all sorts of axioms and spits out all sorts of interesting theorems deriving from these axioms. To deal with these problems, it looks like I'll have to use stuff like pathfinding algorithms with smart heuristics. Now, I seriously doubt my ability to code something like A* in Haskell, in a way that is both simple and efficient, so, I decided to switch to Scala, where I can mix imperative and functional style any way I want.
Ok, that was enough introduction. Here's the code -> http://ideone.com/P2deE
I'd really appreciate it if a (certain) Scala specialist could review the code and tell me how I could make it smaller and / or faster. The code is an almost direct translation of the Haskell version, so, I think there are parts that would be better written in imperative style. For example, I believe the lcnf function could make use of list buffers. Also, about that same function, I tried to implement it like this...
def lcnf(expr: Expr): List[List[Expr]] = {
def lcnfH[T <: Expr](list: List[Expr])(expr: Expr): List[Expr] = expr match {
case T(p, q) => list ::: lcnfH[T](List())(p) ::: lcnfH[T](List())(q) case e => e :: list }
(lcnfH[And](List())(expr)) map lcnfH[Or](List())_
} |
...but it didn't work :/ It seems that I can't pattern match against T. Why? Is there a workaround?
Has anyone else played with stuff like that? If yes, do you have any good (preferably online) studying material I could use?
Finally, if you want, you can help me submit it bug-free to daniweb's code snippet competition. Just try any crazy propositional formula you can think of and tell me if you get a wrong result. I think you can actually do it on the same ideone paste I posted above.
EDIT: Fixed two bugs that caused it to enter an infinite loop for some inputs.
EDIT2: Another bug fix... It should be ok now... I guess...
Last edited on
It seems that I can't pattern match against T. Why? Is there a workaround? |
This is because of the dreaded generic type erasure. Scala 2.10 is going to have some kind of reification to help workaround this. In 2.8 and 2.9 you can use implicit Manifests to let the compiler generate the runtime type information, but this is somewhat hacky.
http://www.scala-blogs.org/2008/10/manifests-reified-types.html
Last edited on
Thanks for the info. I still can't get it to work as I want though >:(
The above gives the compiler a headache. The best I could do was this:
But this is more verbose than the original... I guess I'll have to wait for Scala 2.10...
def lcnf(expr: Expr): List[List[Expr]] = {
def lcnfH[T <: Expr : Manifest](list: List[Expr])(expr: Expr): List[Expr] = expr match {
case T(p, q) => list ::: lcnfH[T](List())(p) ::: lcnfH[T](List())(q) case e => e :: list }
(lcnfH[And](List())(expr)) map lcnfH[Or](List())_
} |
The above gives the compiler a headache. The best I could do was this:
def lcnf(expr: Expr): List[List[Expr]] = {
def lcnfH[T <: Expr : Manifest](list: List[Expr])(expr: Expr): List[Expr] = {
def ret(p: Expr, q: Expr) = list ::: lcnfH[T](List())(p) ::: lcnfH[T](List())(q)
expr match {
case And(p, q) if manifest[T] == manifest[And] => ret(p, q)
case Or(p, q) if manifest[T] == manifest[Or] => ret(p, q)
case e => e :: list }
}
(lcnfH[And](List())(expr)) map lcnfH[Or](List())_
} |
But this is more verbose than the original... I guess I'll have to wait for Scala 2.10...
Last edited on
| The above gives the compiler a headache. |
The above gave me a headache too :P
Anyways, I'd be happy to test it.
closed account (1yR4jE8b)
I've done a bit of Scala myself, but I have no idea what I'm looking at...
Haha, yeah, I guess I should have explained a bit what I'm doing.
Suppose we have to check this propositional formula's validity:
Obviously, this is always true. Either a or b is true [*]. Both a and b imply c. Therefore, in any case, we can infer c. But how can we do that formally? One way to do it is to negate what we want to prove and then try to derive a contradiction. In other words, we can use the well known reductio ad absurdum method. But before we can do this, we have to transform (the negation of) our formula to its so called conjunctive normal form [1]:
What we have now is already in conjunctive normal form:
It is a conjunction (/\) of clauses, where each clause is a disjunction (\/) of literals (a literal is either an atomic formula or the negation of one). We were lucky this time. There is a final step that we didn't have to take here. We could have ended up with something like this:
We'd have to do the distribution to get this:
For (our computer's) convenience, we will change the representation of our formula a bit, using lists:
We are ready to derive a contradiction (or fail to do so) now. The only inference rule we are going to need is resolution [2]. This rule says that if we have p \/ q and ~p \/ r, we can infer q \/ r. We are going to apply it repeatedly to our clause list, and it is guaranteed that either we will derive a contradiction or we will reach a state where we haven't derived a contradiction and we can no longer apply the rule. In the former case, the original formula is valid. Let's see what happens in our example:
And we have just proved that the original formula is valid.
You can see a detailed description of the algorithm here -> [3], in pages 15 - 16.
I hope it's correct, because this is what I used to implement the resolution function.
[1] http://en.wikipedia.org/wiki/Conjunctive_normal_form
[2] http://en.wikipedia.org/wiki/Resolution_(logic)
[3] http://www.cs.nott.ac.uk/~led/papers/led_bsc_dissertation.pdf
[*] Technically, a and b can both be false. But the formula (a\/b) is true iff either a or be is true. And since that formula is supposed to be one of our axioms, it must be true, therefore, either a or b is true.
EDIT: After taking another look at the algorithm description, I think there is one more bug I'll have to fix...
Suppose we have to check this propositional formula's validity:
[(a \/ b) /\ (a => c) /\ (b => c)] => c |
Obviously, this is always true. Either a or b is true [*]. Both a and b imply c. Therefore, in any case, we can infer c. But how can we do that formally? One way to do it is to negate what we want to prove and then try to derive a contradiction. In other words, we can use the well known reductio ad absurdum method. But before we can do this, we have to transform (the negation of) our formula to its so called conjunctive normal form [1]:
[(a \/ b) /\ ( a => c) /\ ( b => c)] => c // original formula ~( [(a \/ b) /\ ( a => c) /\ ( b => c)] => c ) // negate ~( ~[(a \/ b) /\ (~a \/ c) /\ (~b \/ c)] \/ c ) // eliminate implication / equivalency ~~[(a \/ b) /\ (~a \/ c) /\ (~b \/ c)] /\ ~c // push negations inwards, using de morgan's laws |
What we have now is already in conjunctive normal form:
(a \/ b) /\ (~a \/ c) /\ (~b \/ c) /\ ~c |
It is a conjunction (/\) of clauses, where each clause is a disjunction (\/) of literals (a literal is either an atomic formula or the negation of one). We were lucky this time. There is a final step that we didn't have to take here. We could have ended up with something like this:
(a /\ b) \/ (c /\ d) |
We'd have to do the distribution to get this:
(a \/ c) /\ (b \/ c) /\ (a \/ d) /\ (b \/ d) |
For (our computer's) convenience, we will change the representation of our formula a bit, using lists:
(a \/ b) /\ (~a \/ c) /\ (~b \/ c) /\ ~c -> [ [a, b], [~a, c], [~b, c], [~c] ] |
We are ready to derive a contradiction (or fail to do so) now. The only inference rule we are going to need is resolution [2]. This rule says that if we have p \/ q and ~p \/ r, we can infer q \/ r. We are going to apply it repeatedly to our clause list, and it is guaranteed that either we will derive a contradiction or we will reach a state where we haven't derived a contradiction and we can no longer apply the rule. In the former case, the original formula is valid. Let's see what happens in our example:
(1) a \/ b // given (2) ~a \/ c // given (3) ~b \/ c // given (4) ~c // given (5) b \/ c // from (1), (2) (6) c // from (3), (5) (7) false // from (4), (6) |
And we have just proved that the original formula is valid.
You can see a detailed description of the algorithm here -> [3], in pages 15 - 16.
I hope it's correct, because this is what I used to implement the resolution function.
[1] http://en.wikipedia.org/wiki/Conjunctive_normal_form
[2] http://en.wikipedia.org/wiki/Resolution_(logic)
[3] http://www.cs.nott.ac.uk/~led/papers/led_bsc_dissertation.pdf
[*] Technically, a and b can both be false. But the formula (a\/b) is true iff either a or be is true. And since that formula is supposed to be one of our axioms, it must be true, therefore, either a or b is true.
EDIT: After taking another look at the algorithm description, I think there is one more bug I'll have to fix...
Last edited on
A small update.
There are several tasks for a theorem prover that could be greatly simplified with the help of a CAS [1]. For example, suppose we are in first order logic (propositional logic + variables + predicates + functions + quantifiers) and we want to prove the following:
forall(m) : Is2x2Matrix(m) => transpose(transpose(m)) == m
The proof for this could be delegated to a CAS in almost its entirety. The CAS would see the predicate Is2x2Matrix and construct this symbolic representation for m -> {{m1, m2}, {m3, m4}}. Then, it would use the predefined transpose function, and eventually simplify the second part of the implication to true.
Moving from propositional to first order logic is not too much work. The core algorithm is the same, there are just a few more preprocessing steps, so, I decided to focus on building a small CAS / programming language first.
My main concern was "How am I going to implement a type system for this?", as I haven't done anything like this before. After searching for a while, I decided to imitate Mathematica's type system, because it's very easy to implement, because, well, Mathematica doesn't really have a type system. Everything in Mathematica is an expression. Evaluating an expression doesn't yield a value of some type, but another (usually simpler) expression. Expressions have constructors (aka 'heads') that determine how (and if) they interact with other expressions. For example, the expression 1 + 2 + 3 is parsed as Plus[Integer[1], Integer[2], Integer[3]]. The Plus constructor combines its Integer children like this -> Plus[Integer[1 + 2 + 3]], to eventually yield Integer[6]. An expression like this one -> 1 + x, where x is an uninitialized symbol, is parsed like this -> Plus[Integer[1], Symbol[x]]. The Plus constructor doesn't know how to treat this, so, it just leaves it as it is.
Here's my first shot at it -> http://ideone.com/8qLSE
There are still a lot of things to be added (I'm not sure yet what I'm going to implement myself and what I'm going to use existing libraries for), and I think I got carried away and implemented stuff that isn't really necessary, just because it was easy to do so in Scala :D but I believe it's a good start. Any suggestions are welcome and much appreciated.
[1] http://en.wikipedia.org/wiki/Computer_algebra_system
There are several tasks for a theorem prover that could be greatly simplified with the help of a CAS [1]. For example, suppose we are in first order logic (propositional logic + variables + predicates + functions + quantifiers) and we want to prove the following:
forall(m) : Is2x2Matrix(m) => transpose(transpose(m)) == m
The proof for this could be delegated to a CAS in almost its entirety. The CAS would see the predicate Is2x2Matrix and construct this symbolic representation for m -> {{m1, m2}, {m3, m4}}. Then, it would use the predefined transpose function, and eventually simplify the second part of the implication to true.
Moving from propositional to first order logic is not too much work. The core algorithm is the same, there are just a few more preprocessing steps, so, I decided to focus on building a small CAS / programming language first.
My main concern was "How am I going to implement a type system for this?", as I haven't done anything like this before. After searching for a while, I decided to imitate Mathematica's type system, because it's very easy to implement, because, well, Mathematica doesn't really have a type system. Everything in Mathematica is an expression. Evaluating an expression doesn't yield a value of some type, but another (usually simpler) expression. Expressions have constructors (aka 'heads') that determine how (and if) they interact with other expressions. For example, the expression 1 + 2 + 3 is parsed as Plus[Integer[1], Integer[2], Integer[3]]. The Plus constructor combines its Integer children like this -> Plus[Integer[1 + 2 + 3]], to eventually yield Integer[6]. An expression like this one -> 1 + x, where x is an uninitialized symbol, is parsed like this -> Plus[Integer[1], Symbol[x]]. The Plus constructor doesn't know how to treat this, so, it just leaves it as it is.
Here's my first shot at it -> http://ideone.com/8qLSE
There are still a lot of things to be added (I'm not sure yet what I'm going to implement myself and what I'm going to use existing libraries for), and I think I got carried away and implemented stuff that isn't really necessary, just because it was easy to do so in Scala :D but I believe it's a good start. Any suggestions are welcome and much appreciated.
[1] http://en.wikipedia.org/wiki/Computer_algebra_system
Last edited on
Topic archived. No new replies allowed.