Closed wisnesky closed 5 years ago
wisnesky
commented
5 years ago 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
commented
5 years ago 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
commented
5 years ago 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.
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://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://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: