1 ------------------ 2 Otter, Version 3.3 Search for Proofs 3 ------------------ 4 ------------------ 5 Mace, Version 2.2 Search for Countermodels 6 ------------------ 7 8(Also see index.html in this directory.) 9 10---------------- 11OTTER HIGHLIGHTS 12---------------- 13 14Over the years we've added many experimental features to Otter, 15but the basic functions haven't changed much in the past 16ten years. 17 18The Otter package now includes Mace 2 (as a separate program). 19 20---------------- 21Mace2 HIGHLIGHTS 22---------------- 23 24Mace2 is now in independent program. It no longer calls Otter 25to parse the input. It still accepts the same inputs as Otter. 26Performance is sometimes better than in previous versions 27(see mace2/README.22). 28 29---------------- 30DOCUMENTS 31---------------- 32 33The documents directory contains a (newly updated) Otter 3.3 34manual and a Mace 2.0 manual. See documents/README. 35 36---------------- 37FETCHING 38---------------- 39 40Download Otter 3.3 and Mace 2.2 from the Otter Web page: 41 42 http://www.mcs.anl.gov/AR/otter/ 43 44---------------- 45INSTALLING AND TESTING (for unix-like systems) 46---------------- 47 48Unpack the package with a command something like 49 50 % gunzip -c otter-3.3.tar.gz | tar xvf - 51 52Then 53 54 % cd otter-3.3 55 56If you are on a recent linux or Macintosh system, try 57 58 % make install (this just copies pre-compiled binaries to ./bin/) 59 % make test-otter 60 % make test-mace2 61 62Macintosh users: If you see "make: Command not found.", it means 63you don't have the developer's tools (compliers, etc.) installed. 64The good news is that you don't need them. Instead, run the commands 65"./make-install", "./make-test-otter", and "./make-test-mace2". 66 67If test-otter gives a proof and test-mace2 gives a model, everything is 68probably okay. The binaries should be in the directory bin/. 69 70If something goes wrong, try 71 72 % make all 73 74THEN 75 76 % make test-otter 77 % make test-mace2 78 79If any of that fails, see README.make. 80 81To run the Otter test suite, "cd examples; ./Run_all". 82To run the Mace2 test suite, "cd examples-mace; ./Run_all". 83 84The Otter web page is http://www.mcs.anl.gov/AR/otter/ 85 86 W. McCune (otter@mcs.anl.gov) 87 Argonne National Laboratory 88 August, 2003 (updated August 2004) 89