--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/qilang/f80b8110-ee1e-4216-a2d6-7dd5ff62a31en%40googlegroups.com.
The first attempt to tackle Schubert’s Steamroller using unsorted first-order logic was made in the late 1970s with the Markgraf Karl Refutation Procedure (MKRP)—a theorem prover in development at Karlsruhe. In 1978, Christoph Walther and colleagues fed the unsorted axiomatization into MKRP, but it failed to find a refutation sciencedirect.com+8swi-prolog.discourse.group+8d-nb.info+8.
So, to be clear:
MKRP (unsorted resolution) was the first system to try proving the problem without using many‑sorted logic—and it did not succeed en.wikipedia.org+6swi-prolog.discourse.group+6d-nb.info+6.
The first successful automated proof came only later—and only when sorted logic was employed (SAM and Walther’s work in the 1980s).
In short, no system without sorted logic ever solved Steamroller; MKRP was the first to try and the first to fail.
The statement in red is false. I can't find a reference for the first ATP without using sorts to solve this problem; but Prover9 can and Vampire will I'm sure.To view this discussion, visit https://groups.google.com/d/msgid/qilang/bc32a55f-bac8-4cd8-9eb6-f723993b7a38n%40googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/qilang/71c707d5-102f-48b0-b233-cb6c267fcc30n%40googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/qilang/3a407cb3-0378-437f-979d-2a9897945299n%40googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/qilang/3e2224f9-9f66-4483-a028-55f872808569n%40googlegroups.com.
To view this discussion, visit https://groups.google.com/d/msgid/qilang/CAGp%3DqtSX9-or0M6Jd7JCuFHQOehfTbmsO_LWqCXUu6XYnznNyQ%40mail.gmail.com.