SAT Solver

This is a SAT solver for a subset of first-order logic with a slight twist for convenience: instead of specifying one logical formula in conjunctive normal form as is standard, you can write out each component as a separate statement along with a conclusion statement. Rather than joining all the formulas together and checking whether the result is satisfiable, the program leaves them separate, takes the first set as axioms, and determines whether the conclusion can be derived from there. This is logically equivalent to checking for satisfiability, but has the advantage of being able to produce proofs of the conclusion if it's true. Moreover, these proofs will always be the shortest possible proof possible under a given set of derivation rules.

Read on for more on the internals, or check out the source.

How does it work?

At a high level, the program can be broken down into two steps: parsing and searching. The parse step simply breaks down the unstructured human input into a formal structure for the computer to use. The search step functions by the following procedure:

Add all given axioms to a list of things known to be true.
Pair each truth with a derivation showing how it's known to be true (in the beginning, this is just "it was given as an axiom" for each).
Check if the conclusion is known to be true. If so, output this and end the program.
For each true statement found so far, apply every applicable logical rule to get a new set of truths.
Add these new truths to the list of truths along with the rule to derive them.
Return to step 3.

Grammar

The syntax is pretty straight forward to grasp from example, but for completeness here's a simple formal spec:

nat ::= 1 | 2 | 3 | ... | infinity
atom ::= A | ... | Z

statement ::=
	| (statement)
	| -(statement)
	| +upperterm+upperterm
	| +upperterm+upperterm
	| -upperterm+upperterm
	| -upperterm-upperterm

upperterm ::=
	| atom
	| upperterm*
	| (innerterm)

innerterm ::=
	| upperterm
	| -upperterm
	| compoundterm

compoundterm ::=
	| +upperterm+upperterm
	| +upperterm+upperterm
	| -upperterm+upperterm
	| -upperterm-upperterm

Further Explanation

An argument is composed of a series of premises expressed as statements followed by a conclusion statement prefixed with a slash. Each statement is written on its own line. Four types of statements are supported:

	Affirmative	Negative
Universal	-T+T	-T-T
Particular	+T+T	+T-T

The letter T above denotes a term, which is discussed below. The quality of a statement can be either affirmative or negative (+ or -) and the quantity either universal or particular (- or +). Below are some examples corresponding to the four types of statments you can get from these:

	Affirmative	Negative
Universal	All cows eat grass	All cows don't eat grass
Particular	Some cows eat grass	Some cows don't eat grass

Terms

There are only two types of terms in the DSL, atomic and compound.

Atomic Terms

Atomic terms are written with a single uppercase letter. They represent only themselves as symbols in the logic and can be given whatever semantic meaning is fitting for the context of the problem. For example, you could use C and G to represent "cows" and "grass" in the above examples when translating them into the DSL:

	Affirmative	Negative
Universal	-C+G	-C-G
Particular	+C+G	+C-G

Compound terms

Compound terms are just combinations of other terms, which can be nested arbitrarily deep, such as +(-(+A+B))+C. Any term can be negated with a minus sign. For example, +C-G is logically equivalent to +C+(-G) (i.e. "Some cow doesn't eat grass" means the same thing as "Some cow eats only non-grass").

Implementation

The backbone of the code is written in OCaml, which, being a variant of ML, is unsurprisingly well-suited to a task like this. The parser is a hand-rolled recursive-descent parser, since I was learning about parsers and thought it would be cool to write a small one rather than use a library, especially given that the grammar's not all that involved.

If you've read to here, then I'm shocked and surprised. Go take a look!.