[Haskell-cafe] ANN: theoremquest-0.0.0

[rusi]

On Feb 28, 7:59 pm, Tom Hawkins <tomahawk... at gmail.com> wrote:
> I have been wanting to gain a better understanding of interactive
> theorem proving for some time.  And I've often wondered: Can theorem
> proving be made into a user-friendly game that could attract mass
> appeal?  And if so, could a population of gamers collectively solve
> interesting and relevant mathematical problems?
>
> To try to answer these questions -- and to gain some experience myself
> with theorem proving -- I started a project called TheoremQuest [1].
> TheoremQuest intends to be a multi-player game system, where the game
> server receives requests by clients, such as theorem queries and
> inference rule applications.  The TheoremQuest server validates
> deductions, compares them with existing theorems in the database, then
> returns results.  TheoremQuest's deductive system borrows that of John
> Harrison's HOL Light [2].
>
> There are 2 Hackage packages:  theoremquest [3] is a library that
> declares types for terms, inference rules, and client-server
> transactions, used by both server and clients; and theoremquest-client
> [4] is an example client (tq).  All the code, including the
> server-side, is hosted at github [5].
>
> Currently the client-server interface is working, but little else.
> The library has defined most of the core inference rules, but has none
> of the basic types or axioms.  And the "tq" client is nothing at all
> like a game; at this point it is just a command line tool to test the
> server.  Currently "tq" can ping the server, create a new user, apply
> inference rules, and print out theorems.  Here's how "tq" can prove "x
> |- x":
>
> $ tq newuser tomahawkins tomahawk... at gmail.com
> Ack
> $ export THEOREMQUEST_USER=tomahawkins
> $ tq infer 'ASSUME (Var (Variable "x" Bool))'
> Id 1
> $ tq theorem 1
> assumptions:
> Var (Variable "x" Bool)
> conclusion:
> Var (Variable "x" Bool)
>
> I'd love to have help with this project, if anyone's interested.

I am curious -- how easy is it to use theoremquest for playing with
equational theories?

In particular equational logic -- see

https://www.ideals.illinois.edu/bitstream/handle/2142/11411/A%20Rewriting%20Decision%20Procedure%20for%20Dijkstra-Scholten%27s%20Syllogistic%20Logic%20with%20Complements.pdf?sequence=2