Chapter 10 requires Mace4 and Prover9 but they appear to be unavailable

[AncientZygote]

I see that you have deleted a couple of references to Prover9 in Chapter 10, but many of the examples do require a theorem prover in order to execute, i.e., the nltk/inference module does not seem to have a replacement for Prover9. I see a general purpose api in the inference module but it does not appear to have an explicit prover executable specified. Is it possible to substitute the Tableau Prover in tableau.py (will check that later but thought I would mention it now)?

In a similar vein, Chapter 10 requires a model builder to execute examples such as given in Section 5.2 using nltk.DiscourseTester. Mace4 seems not to be available anymore at https://www.cs.unm.edu/~mccune/mace4/ (there is a very old installer available for Prover9 and Mace4 with a gui but it uses MSVC runtime (MSVCP71.DLL) from many years ago (apparently the installer was last compiled 2007) and I am wary of using it. I simply wanted the command line version of Prover9 and Mace4 that may still be available for Linux/Apple as LADR, but seems not to be available for recent Windows OS.

This issue is not a show stopper, i.e., the course material is understandable without Prover9 and Mace4 but it would be nice to have alternatives to them in order to follow the examples completely.

[stevenbird]

@ewan-klein do you have any advice please?

[AncientZygote]

Section 3.8 Model Building from Chapter 10 could be revised such that Mace4 is no longer discussed. It would be relatively painless to simply discuss model building and the significance of models in QL, i.e., that truth in QL is truth in a model, etc. (there is an excellent discussion of models in Chapter 5 of Forallx - An Introduction to Formal Logic by P.D. Magnus (freely available under a Creative Commons license). For the purposes of NLTK it seems that the main point is that a model builder can be used to construct a countermodel and act as an adjunct to a prover (the prover seeking to find a proof of first order statments and a model builder seeking to find a counterexample).

More problematic is the fact that your discourse.py relies on the mace module for consistency checking of discourse structure, i.e., discourse testing. I don't know of a substitue for Mace4 at the moment, but I am new to the field. Chapter 10, Section 5.2 Discourse Processing seems fairly dependent on having Mace4 available to provide discourse testing and incrementally check the model whenever a new sentence is added to the discourse thread (affecting nltk.DiscourseTester and its methods reading and add_sentence, for example).

Possibly Section 5.2 could discuss discourse processing in the context of named entity recognition and coreferences, i.e., in the context of services available in the Stanford CoreNLP package, though that package is not beginner oriented and the NLTK interface template in stanford.py (of the NLTK package) would probably not be a good path for integration with CoreNLP because it appears to use piping, bringing up CoreNLP parser instances in Java from Python, which is tricky when you potentially have 32 bit java base and 64 bit Python (which is more likely these days).

I personally have done some preliminary testing using CoreNLP as a local http server so can query its services via http posts and obtain output via http or have it write to a file which I can then open from NLTK/Python without concerns about differing runtime environments (there are other ways to accomplish this, e.g., running a Java virtual system, but I am skeptical of that for normally endowed machines, since CoreNLP barely runs a minimum set of available services with 1.5 GB memory allocated, so you really have to serialize and run consecutive batches, which CoreNLP is designed to be anyway, i.e., a pipeline for various language processing tasks.

I hope this gives you some possible paths to deal with the Prover9 and Mace4 availability problem in the NLTK book. I spent a few hours yesterday working with NLTK tableau.py and it seems to have not been quite completed as production code (as a prover), having a number of sample input FOL statements commented out as non-functional and it wouldn't run the higher order tests for me (testHigherOrderTableauProver in tableau.py). I am trying to troubleshoot that, but it is pretty nitty gritty and I am planning today to look at tableau provers generally and see if that gives me a stronger analytic stance in looking at tableau.py. I was hoping it might be a substitute for Prover9 at least in the examples required for Chapter 10. I will keep you posted on that analysis (of whether you might substitue tableau.py prover services for Prover9 in Chapter 10 examples).

[AncientZygote]

Believing that Prover9/Mace4 was no longer available for Windows users, I had hoped to present an alternative to Prover9/Mace4 to support theorem proving and model checking in the NLTK context (discussed in earlier post). Towards that end I have spent a few hundred hours working with the Isabelle, an environment for constructing formal mathematical proof in human-readable form. You can do quantified logic theorem proving and model checking with Isabelle, e.g.,

lemma "(∃ x. (Man(x) ∧ Walks(x))) ∧( ∃ y. ( Mortal(y) ∧ ¬Mortal(y) ))" nitpick [ falsify = false ]

proof (prove) goal (1 subgoal):

1. (∃x. Man x ∧ Walks x) ∧ (∃y. Mortal y ∧ ¬ Mortal y) Nitpicking formula... Timestamp: 00:19:06. Formula: (Man ??.sk0@1_x ∧ Walks ??.sk0@1_x) ∧ Mortal ??.sk0@2_y ∧ ¬ Mortal ??.sk0@2_y. The types 'a and 'b passed the monotonicity test. Nitpick might be able to skip some scopes. Nitpick found no model. Total time: 11.3 s.

Nitpick correctly found no model because that set of assumptions is contradictory. Nitpick, written for Isabelle/HOL, builds on the MIT first-order relational model finder Kodkod (using a third-party Java front-end called Kodkodi, included in the Isabelle distribution) and invokes one of the SAT solvers included in the Isabelle distribution (I used SAT4J in the above Isabelle session). However, it does require quite a bit of work to become familiar with the Isabelle environment. Despite the recent work, I have barely scratched the surface of using Isabelle. You can use a command line interface and bypass the jEdit interactive environment, but I have not attempted that yet. Isabelle also permits custom ML code (its ground level machinery is written in ML) so there seems to be a ready path for custom applications.

I have good news for those who, like me, are working in a Microsoft Windows environment with NLTK. I downloaded the old Prover9-Mace4 Graphical User Interface version at (https://www.cs.unm.edu/~mccune/mace4/gui/v05.html). This is the software I had been concerned about using because it required a very old MSVC runtime dll (a link to obtain that dll was provided, but I wondered whether there might be problems nonetheless in current Windows operating system environments some 10 years subsequent to that dll context). Also, it was not clear whether the gui version would permit command line access, as required for the integration with NLTK (see earlier posts in this thread).

I am happy to report that I ran the gui installer, which placed the Prover9-Mace4 program in the Windows C:\Program Files (x86)\ directory. I did not bring up that program, but instead looked for the command line versions, which were indeed in a subdirectory, \Prover9-Mace4\bin-win32.

I created a Microsoft Windows system environment variable, PROVER9, and set its value to the subdirectory containing the Prover9/Mace4 command line binaries: C:\Program Files (x86)\Prover9-Mace4\bin-win32. I then brought up NLTK in a Python IDLE session and successfully ran the NLTK book Chapter 10 examples requiring Prover9 and Mace4.

I note that in the process of testing Prover9/Mace4 with Chapter 10 NLTK book, I discovered that the NLTK distribution does not include the Malt dependency parser (http://www.maltparser.org/), necessary to using the Glue Semantics in the NLTK discourse module. I will investigate whether that parser is available at the link given and whether it will still interface with NLTK (with some help pointing NLTK at it presumably).

I do believe that in the long run it would be very useful to include examples of using the Isabelle software in Chapter 10, since it permits mathematically rigorous evaluation of theoretical models that underpin much of the NLTK presentation of natural language, semantics and logic, i.e., a student might be able to take knowledge of Isabelle along in advanced applications later in their careers. For example, Isabelle was used by Hewlett-Packard in the design of the HP 9000 server and discovered a number of bugs that had escaped previous formal testing and simulation. Isabelle is also, of course, used to formalize theorems in mathematics and computer science generally, which might be an asset in the design of industrial grade natural language processing applications (as well as providing an enduring adjunt to NLTK).

I would say the original issue of this thread can be closed, but I will leave it open for a time to assure the information propagates (I am still becoming familiar with the Github environment). Well, I guess I will close it, since the "close and comment" button did just that.

[joycehuang8888]

set PROVER9=\Prover9-Mace4\bin-win32 works for me.

[chansonzhang]

I created a Microsoft Windows system environment variable, PROVER9, and set its value to the subdirectory containing the Prover9/Mace4 command line binaries: C:\Program Files (x86)\Prover9-Mace4\bin-win32. I then brought up NLTK in a Python IDLE session and successfully ran the NLTK book Chapter 10 examples requiring Prover9 and Mace4.

As I was usging pycharm, a pycharm restart is needed after the environment PROVER9 have been set.

[BrazilForever11]

Downloading GUI and dll and setting window environment variable worked. But I feel there should be issue open on replacing Prover9 with Isabelle or something similar. Can we reopen this one or create new issue?