Online (or off the shelf) Knuth-Bendix tool

Stream: Equational

[Fan Zheng]

Does anyone know an online or one-click-to-install Knuth-Bendix tool that doesn't hang if the process doesn't terminate; instead it will output a list of critical pairs found so far and pause for the user to examine and decide whether to continue, abort or modify the original problem.

[Shreyas Srinivas]

Kbcv

[Bhavik Mehta]

Kbcv hangs if the process doesn't terminate

[Fan Zheng]

Right, I have crashed a bunch of tags on that one.

[Bhavik Mehta]

You have the option of pressing "completion" in the local installation version, then pressing stop after 5 minutes, and examine there. But I realise this isn't exactly what you ask for, plus the install requires a working scala installation, so it's not one-click either

[Fan Zheng]

OK, so I relax my condition of one-click, but insist that it should run on Windows.

[Michael Bucko]

Btw. I forked and translated this repo https://github.com/curegit/knuth-bendix-completion here:
https://github.com/riccitensor/deeppattern

And wrote this in OCaml: https://github.com/riccitensor/deeppattern/blob/master/check_implication.ml

You can use dune to build it. It so far did not solve what I wanted, but I found this tool interesting, so I am experimenting with OCaml + term rewriting + Knuth-Bendix completion.

[Cody Roux]

I wrote this a short while back, but I don't know that it's bug-free: https://github.com/codyroux/knuth-bendix

[Cody Roux]

It's OCaml + term rewriting + Knuth-Bendix completion :)

[Cody Roux]

The other tool looks nicer though...

[Michael Bucko]

Cody Roux schrieb:

I wrote this a short while back, but I don't know that it's bug-free: https://github.com/codyroux/knuth-bendix

Ah, really cool. Gonna check it out! Love OCaml!

[Michael Bucko]

Cody Roux schrieb:

The other tool looks nicer though...

Looked nice, but had no stars, and had to translate it using GPT4. Runs quite immediately, but it might be buggy, too.

[Eric Taucher]

A long time ago worked with some others to translate "Handbook of Practical Logic and Automated Reasoning" by John Harrison (site), OCaml code to F# which includes the Knuth-Bendix algorithm

https://www.cl.cam.ac.uk/~jrh13/atp/OCaml/completion.ml

The F# code is here (GitHub) and was verified against the OCaml results however the F# code no longer runs as posted in GitHub do to updates with F# and such.

[Eric Taucher]

For Knuth-Bendix code that is part of HOL-Light (GitHub) and seems be based on the above noted OCaml code

https://github.com/jrh13/hol-light/blob/master/Examples/kb.ml

A search for Knuth in the HOL-Light code also returned this

https://github.com/jrh13/hol-light/blob/master/metis.ml#L7253