Knuth-Bendix (KB) prover

[wisnesky]

No description provided.

[wisnesky]

In Prover.hs there is a datatype

data ProverName = Free | Congruence | Orthogonal | KB | Auto

Free and Orthogonal are already implemented. The goal here is to implement KB (i.e., fill in all existing missing case statements for ProverName) using the Twee library:

http:https://hackage.haskell.org/package/twee

Also, the "KB" example or something similar from AQL-java should be added to the test suite.

I've been in contact with the author, Nick Smallbone. He had this advice:

Twee is intended to be usable as a library - I use it like that in QuickSpec (http:https://hackage.haskell.org/package/quickspec). But since I'm the only person using it like that, the API exposes somewhat too much of Twee's internals and is very underdocumented. But I'm happy to help you get your head round it :)

The main restriction at the moment is that the only term ordering supported is KBO. I've been meaning to add other term orderings so, if that's a problem, let me know and I'll see what I can do.

The main completion loop is the function Twee.complete in the package twee-lib. It has the type

complete :: (Function f, MonadIO m) => Output m f -> Config f -> State f -> m (State f)

(there is also a pure variant completePure), where:

• f is the type of function symbols, which you have to define yourself (see below).

• Output m f is called to display progress messages.

• Config f is the prover configuration. You can get a default configuration with defaultConfig and then customise it by updating the fields. There is no way to set a timeout at the moment (I could add one if you need it) but you can set the cfg_max_critical_pairs field to stop after a certain number of critical pairs are generated.

• State f is the prover state and contains both the rewrite rules found so far and the set of unprocessed critical pairs. initialState gives you an empty prover state (no equations and no rewrite rules). You can use addAxiom to add the input equations to it.

complete runs until either the equations are completed, the goal (if any) is proved or a resource limit is reached. The function rules :: Function f => State f -> [Rule f] then gives you the generated rewrite rules. There isn't a built-in function for checking if completion succeeded (rather than reaching a resource limit) but I think the following code should work:

successful :: State f -> Bool
successful = isNothing . fst . dequeue

The API for manipulating terms is in Twee.Term and uses a builder interface which might take a bit of getting used to. Here are a few examples:

-- Building the term f(X, c)
t = build (app (fun f) [var x, con (fun c)])

-- Pattern matching on the above
App (F f) (Cons (Var x) (Cons (App (F c) Empty) Empty)) = t

-- Instead of using Cons and Empty, you can use unpack to unpack an argument list
App (F f) ts = t
[Var x, App (F c) Empty] = unpack ts

Finally, you will need to define the type of function symbols. This can be whatever you want but needs to implement several typeclasses which can all be found in Twee.Base. You should make your function symbols have type 'Extended f' (Extended is also defined in Twee.Base) in order to get several of these instances for free. That is, the prover state will have type State (Extended MyFunctionSymbol). You will need to define the following instances:

• Ord - defines symbol ordering for KBO
• Size - defines symbol weight for KBO
• Arity - gives the arity of each function symbol
• Ordered - defines the term ordering. Define it as follows:
  import qualified Twee.KBO as KBO
  instance Ordered MyFunctionSymbol where
  lessEq = KBO.lessEq
  lessIn = KBO.lessIn
• Pretty - for pretty-printing function symbols.
• PrettyTerm - lets you customise pretty-printing, e.g. to choose whether terms are printed curried or uncurried. You can leave the instance body blank to get the default behaviour.
• EqualsBonus - just leave the instance body blank.

[wisnesky]

I hooked this up, but I'm now waiting on a few questions from the author about how to infer symbol precedences and weights. For now this prover just loops forever almost always.

[wisnesky]

Apparently twee doesn't do completion of an equational theory T and yield a decision procedure; it decides T -> t by deciding !t /\ T -> true = false using the usual method of skolemizing t and axiomatizing Boolean logic. That will make things harder.

[wisnesky]

Re: above, twee seems to work if we re-complete with a new goal every time we're asked to decide an equality. Highly inefficient, although slightly more general that using completion straight up.