-
Notifications
You must be signed in to change notification settings - Fork 11
/
Changelog.old
1595 lines (1264 loc) · 60.8 KB
/
Changelog.old
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
-------- LADR 2009-11A ----------
November 4, 2009.
Online Examples. Somewhere along the line, the XML/XSL/HTML
rendering of the tables for interpretations broke in Firefox
(ok in Safari, don't know about IE). I suspect it's a Firefox
problem, because using xsltproc separately to translate
the XML to HTML produces HTML that Firefox renders correctly.
This is beyond me. Help?
November 3, 2009.
Newauto. Oct 1 fix causes big slowdown in fof-prover9 jobs
that spawn hundreds of children. Undo that fix and fix it in
a different, kludgey way by inserting "flip_matches_hint" into
symbol table at start of forking_search. Any other lables that
might be introduced by children should be handeled similarly.
November 3, 2009.
Prover9, Mace4, LADR. Change default max_megs from 200 to 500.
This also affects other LADR programs like prooftrans.
October 28, 2009.
Prover9. Bug appears when using prolog_style_variables with
weighting rules: the special symbol "_" in weighting rules
is treated as an ordinary variable. Fixed by changing the definition
of prolog_style_variables so that they don't include symbols
that start with "_".
October 1, 2009.
Newauto. Bug appears when child search introduces new hint label
("flip_matches_hint"). Fix by changing new_symbols_since_mark()
(in ladr/symbols.c) so that *all* new symbols are reported.
July 9, 2009.
Prover9. Very minor bug: at top of proof, the line "Maximum clause
weight" always prints integer, even if floating-point. Fixed.
June 29, 2009.
Ladr_to_tptp. Bug causes $F ("false" in LADR) to be treated as
a constant. Fixed so that it translates to $false ("false" in TPTP).
May 22, 2009.
Prover9. Bug in production mode when compiled for 64-bit computers.
Line 103 in ladr/dollar.c: sizeof(int) should be sizeof(void *).
Fixed.
April 9-10, 2009.
apps.src. New program to generate constant definitions for TRC
experiments: gen_trc_defs.
LADR: flat demodulation: when clearing substitutions, also check
and clear "alternative" field. This fixed a problem caused by
nonstandard use of flatterms in new app gen_trc_defs; the change
should not affect prover9.
March 17, 2009.
Interpformat and Isofilter: would crash in some cases when
the Mace4 job used op commands to declare print/parse properties.
Fixed by introducing "simple_parse" flag in parse.c. This
avoids problems when special symbols are used in standard
prefix form, e.g., interps in standard form.
March 12, 2009.
Mace4. Bug (segfault) in some cases when input formula
simplifies to $T or to $F. Fixed.
February 26, 2009.
Prover9. Production mode bug: segfault when doing arithmetic
(op_code out of range in rewrite). Fixed.
-------- LADR 2009-02A ----------
February 1-24, 2009.
Prover9. New "production mode" which uses hyperresolution
along with new rewriting system (conditional rewrite rules
and ability to rewrite atomic formulas) to do things like
forward-chaining state-space searches. See the HTML manual
"More Features -> Production Mode".
February 19, 2009.
Prover9. New parm eval_var_limit (for semantic guidance).
This simply changes eval_limit based on the size of the
largest interpretation. See the manual.
January 25-26, 2009.
Prover9. Preliminary work on extending hyperresolution for
evaluable antecedents and consequents.
January 21, 2009.
LADR. The October 21 change of giving "--" built-in parsing
property op(500, infix, "--") took away the ability to write
terms like --x (without space) using unary minus. I think this
important, so I'm rescinding that Oct 21 change. The "--"
symbol was used for binary minus in the Mace4 built-in arithmetic,
so from now on, we'll have to write, e.g., "x + -y" instead
of "x -- y". (Symbols in LADR cannot be overloaded, so we cannot
use "-" for both unary negation and binary minus.)
LADR has been updated so that it no longer accepts "op"
declarations for "--", "---", "----", ... . Also, it no longer
accepts declarations for "''", "'''", "'''", ... . These are
special-case restrictions so that the prefix operation "-"
can be input and output without space for nested occurrences,
e.g., "--x = x". Similarly, for postfix operation "'", e.g.,
"x'' = x".
Unfortunately, this change messes up the programs tptp_to_ladr
and ladr_to_tptp, because they rely on an operation "--".
A kludge gets around the problem.
January 20, 2009.
Prover9. A new experimental feature was enabled by mistake:
assign(complexity, 1). This causes clause weights to get
floating-point values by default. It has been disabled.
-------- LADR 2009-01A ---------- (unannounced)
January 15, 2009.
Mace4. Bug (reported bu Peter Jipsen) when using set(skolems_last):
it can miss some (nonisomorphic) models. Fixed.
Prover9. Minor change requested by Bob Veroff: hints count message.
Newauto. Minor change requested by Veroff: change prepend to append.
December (mid).
Prover9. Complexity function for weighting (preliminary work).
assign(complexity,1) breaks ties when selecting given clauses,
based on a complexity measure: more complex has lower weight.
Not in the manual.
December 11, 2008.
Mace4. User-declared skolem functions do not work with skolems_last
option. Fixed.
-------- LADR 2008-11A ----------
November 15, 2008.
Mace4. New option set(arithmetic) builds in some integer arithmetic.
See the Prover9 HTML manual.
November 7, 2008.
Mace4. Previously, a domain element out of range would always
cause a fatal error, even if higher domain sizes had been specified.
Now, it will simply skip the domain size and try the next size.
October 26, 2008.
Prover9. Bug when action, triggered by kept-clause-count,
asserts a clause, e.g., kept = 10 -> assert(-p | a | b).
(reported by Ken Kunen). Clause is asserted repeatedly
until segfault. Fixed by moving one line of code. I can't
understand why that line of code was where it was; if there
was a good reason, this fix might cause some other problem.
October 23, 2008.
LADR. New type of option is accepted: "floatparm". This allows
assignment of floating-point values to some of the parameters,
e.g., assign(max_weight, "10.2"). Floating-point values must be
enclosed in double quotes.
Prover9. Floating-point values can be used for the parameters that
control weighting: max_weight, variable_weight, constant_weight,
not_weight, or_weight, sk_constant_weight, prop_atom_weight,
nest_penalty, depth_penalty, var_penalty, default_weight.
Integers can still be used for these. Also, weighting rules
can have floating-point values (in double quotes) as well as
integers.
October 23, 2008.
Prover9. Parm skolem_penalty has been removed; it was for an
experiment, and it never made much sense.
October 21, 2008.
Mace4. New flag order_domain builds in the relations < and <=
(less-than, less-than-or-equal) on the members of the domain
(in the same way that the flag integer_ring builds in the
operations +,*,- as the ring of integers mod n).
Also, when integer_ring is set, the operation "--" is
built-in as binary minus. (So you can write x -- y instead
of x + -y.)
Mace4. Accepts new list, list(distinct) to say that lists of
objects are distinct. E.g.,
list(distinct). [a,b,c]. [d,e]. end_of_list.
is shorthand for
formulas(assumptions). a!=b. a!=b. b!=c. d!=e. end_of_list.
LADR. "--" and "++" get built-in parsing properties:
op(500, infix, ["--", "++"]).
October 18, 2008.
Interpformat. Add option "wrap" which encloses interps in
list(interpretations). ... end_of_list.
October 10, 2008.
Prover9. Change hints matching so that non-orientable equality
units are tried both ways when looking for a matching hint.
When the flip matches a hint, append a label "flip_matches_hint"
to the clause.
October 7, 2008.
Ladr_to_tptp. Yet more changes. More parentheses output.
New command-line options: -p says to output all parentheses.
-q says to single-quote unacceptable TPTP symbols, e.g., x*y
becomes '*'(x,y) instead of tptp0(x,y).
Tptp_to_ladr. New command-line option: -q says to double-quote
unacceptable LADR symbols.
October 2, 2008.
Prover9. Bug: assign(demod_size_limit, -1) is supposed to mean
infinity, but it doesn't. It causes demodulation to stop
prematurely. While looking at this, we decided that a better
parameter would be demod_increase_limit, which would terminate
demodulation when the size (symbol count) of the clause increases
more than the limit. So demod_size_limit is eliminated, and
demod_increase_limit (default 1000) is introduced. Also, the
warning messages about demod_step_limit and demod_increase_limit
have been improved.
-------- LADR 2008-09A ----------
August 30, 2008.
LADR. clause_ident failed to check sign when checking identity
of literals. Fixed. That routine is used in several places;
prooftrans caused the bug to appear (missing hints).
August 28, 2008.
Changelog. Reverse so that most recent entries are at the beginning.
August 27, 2008.
Prover9 Manual. It incorrectly said that max_weight=-1 means
infinity (no limit). Fixed.
August 22, 2008.
Prooftrans, Directproof. These failed if the empty clause has
an answer attribute with more than 1000 characters (buffer limit,
not buffer overrun). Fixed.
Prooftrans. Previously, the order of the arguments "expand" and
"renumber" was irrelevant; it always expanded first. Now, it
does the transformations in the order given on the command line.
August 18, 2008.
Prover9. Hint degradation: weights were artificially high,
because the number of previous matches included clauses that
were later forward subsumed. Fixed.
Prover9. When generating Skolem functions, allow them to
to occur in the hints list. When building up sets of hints
by iteration, this change prevents generating new Skolem
functions in each search. This involved substantial changes
to code in symbol_check_and_declare. The routine accept_list
takes an additional argument.
August 14, 2008.
Prover9. Force evaluation (w.r.t. semantics) just before
clauses are "kept". Previously, clauses were evaluated only
when needed by keep/delete rules or given-selection rules.
The change makes sure false clauses have the "false" label
if print_kept prints them.
Prover9. Crash if sos is full (sos_limit) and all are high
priority (e.g., hints), because a "worst" clause cannot be found.
Fix: allow "worst" clauses to be high priority.
-------- LADR 2008-08A ---------- (unannounced)
August 5, 2008.
Prover9: Another incompatibility of lex_order_vars with KBO.
For example, with lex_order_vars, m(x,y,z) < m(z,y,x), but NOT
m(x',y,z') < m(z',y,x'), because, although x and z are
comparable, but x' and z' are not. A patch: when trying
to compare f(alpha) and f(beta), go right to comparing
alpha and beta, rather than checking the variable condition.
This fixes this particular problem, but there may be similar
ones lurking.
(The change applies also without lex_order_vars, but it should
not change the behavior in that that case.)
Tptp_to_ladr: stupid inefficiency in list processing causes
inputs with many formulas to take a very long time. Fixed.
-------- LADR 2008-07A ---------- (unannounced)
July 9, 2008.
All code: get rid of variable declarations that are not at the
beginning of a block. (To satisfy old compilers.)
-------- LADR 2008-06A ----------
June 23, 2008.
Prover9. Produce more output during preprocessing. Previously,
in the section "CLAUSES FOR SEARCH", there could be justifications
like [back_rewrite(9),rewrite([11(3)])], with clauses 9 and 11
not appearing before that point, because they had already been
disabled, e.g., by back rewriting. Now, most clauses that get
IDs during preprocessing are output (if print_initial_clauses is set).
June 21, 2008.
LADR (ladr_to_tptp and tptp_to_ladr). The May 14 changes caused
a problem: operations of different parse types with the same
precedence:
declare_parse_type("|", 502, INFIX_RIGHT);
declare_parse_type("~|", 502, INFIX);
declare_parse_type("&", 503, INFIX_RIGHT);
declare_parse_type("~&", 503, INFIX);
This is not allowed in LADR. Solution: don't support ~| or ~&.
June 12, 2008.
Prover9. Remove the May 18 weighting code (too slow and broken).
New code: allow a user/programmer to write weighting functions in C,
and then refer to the new function, say func42, in weighting rules
like this: weight(f(x,y) = call(func42,x) + weight(y).
See the new source file ladr/weight2.c.
Prover9. Suppress selector_report in "Low Water" messages, unless
assign(stats, all).
Prover9. Bug with assign(sos_limit, -1). (E.g., clear(auto_limits)).
-1 is supposed to mean infinity, but Prover9 was interpreting
is as a small limit, causing sos_empty. Fixed.
June 11, 2008.
Prover9. Bug reported by Michael Beeson. Unit deletion, in which the
unit contains an answer attribute with variables: variables do not get
instantiated. Fixed.
Prover9. Another (minor) answer literal bug: When a proof has answers,
a message containing the answer goes to stderr and at the start of
the proof. When there were multiple answers, only the first was
printed. (The empty clause at the end of the proof correctly printed
all answers.) Fixed.
May 18, 2008.
Prover9. Experiment to allow weighting function to call an external
program to compute the weight. Works on Mac (very slowly), fails in
linux (system call popen() works differently.)
-------- LADR 2008-05B ----------
May 15, 2008.
Prooftrans. Added Bob Veroff's "tagged" output format. This involved
some new code in ladr/{just.c,ioutil.c}.
May 14, 2008.
LADR (ladr_to_tptp and tptp_to_ladr). Several changes (from
Geoff Sutcliffe) on parse/print declarations: "=>" and several
other TPTP operations changed from INFIX_RIGHT (xfy) to INFIX (xfx).
-------- LADR 2008-05A ----------
May 7, 2008.
Prover9. The weighting rules now can include a vars(term) operation,
which is the number of (distinct) variables in the term.
This is analogous to the depth(term) operation.
Prover9. The SELECTOR REPORT is printed only with assign(stats,all).
Prover9. When a kept clause does not match any given_selection
rules, a warning is printed (previously, it caused a fatal error).
Fof-prover9. Efficiency bug when there are many (>50) subproblems
having to do with new symbols. Fixed by considering function/relation
symbols only.
April 23, 2008.
Prover9. Bug in new given_selection code: "positive" is true
if any positive literals. Same for "negative". Fixed.
This bug also affected list(keep) and list(delete).
April 14, 2008.
Expand_proof bug (called by prooftrans, directproof) occurs for
assert-by-action with immediate simplification. It was producing
justifications like [assumption,rewrite...]. Expand_proof could
not handle it. Instead of fixing expand_proof, the assertion
was changed so that if it is immediately simplified, a "copy"
inference is inserted. The reason: [assumption,rewrite...]
in a proof is bad, because you don't see what the actual
assumption is.
April 13, 2008.
Directproof. Bug causes coredump. Trivial case not handled:
flip negative equality, then implicit resolution with x=x. Fixed.
-------- LADR 2008-04A ----------
March 24--28, 2008.
LADR. New language to specify clauses by various properties.
For example, "weight < 40 & (horn | variables = 3)". This
will be used for deciding which clauses to keep and for selecting
given clauses. See next paragraph.
Prover9. Use the new language in three ways:
(1) list(keep). <clause_property_expressions> end_of_list.
(2) list(delete). <clause_property_expressions> end_of_list.
(3) list(given_selection). ... end_of_list.
See the HTML manual (new sections "Advanced Features").
list(delete) is a generalization of max_weight, max_vars, etc.
list(given_selection) is a generalization of weight_part, age_part,etc.
Max_weight, weight_part, etc. will still be accepted, but those
operations will now be implemented by the new mechanisms.
These are big changes to Prover9, and there are probably some bugs.
The way sos_limit works has been changed. It has always been
an ad hoc heuristic, and it still is, but it is now simpler.
Warning: searches that use sos_limit *will* behave differently
in the new Prover9. The new parm sos_keep_factor adjusts
how sos_limit works.
New naming convention for releases.
March 21, 2008.
Prover9. Minor bug involving lex_order_vars and hints.
Fix: renumber variables in hints, just after orienting and
before indexing (also for back-demodulated hints).
-------- LADR March-2008A ---------- (unannounced release)
February 28, 2008.
Prover9. Bug involving hints with sos_limit. Clauses matching
hints (i.e., really good clauses) were being deleted by sos_limit
to make room for clauses that might not be as good. Also, this
bug can cause clauses to be inferred, kept, deleted, inferred,
kept, deleted, ... . Fixed.
February 19, 2008.
Tptp_to_ladr. The Feb 14 precedence change (~) was no good.
After discussion with Geoff and Josef, we decided that the
previous precedences were okay, so undo the Feb 14 change.
-------- LADR Feb-2008B ---------- (unannounced release)
February 15, 2008.
LADR. Give a better error message (and catch the error sooner)
if variables are used as atomic formulae, e.g.,
xor(x,y) <-> ((x & -y) | (-x & y))
February 14, 2008.
Clausefilter. Accept new command-line option "ignore_nonevaluable"
which says to skip evaluations when the formula contains symbols
not in the interpretation.
Tptp_to_ladr. Change precedence of ~ (TPTP spec changed).
February 8, 2008.
Prover9. Fix default_parts bug (clearing does nothing) introduced
on Jan 29.
-------- LADR Feb-2008 ---------- (unannounced release)
February 4, 2008.
Prover9. New action "assert(some_clause)" causes the clause
to be generated and processed when the action is triggered,
e.g., list(actions). given=100 -> assert(x*y=y*x). end_of_list.
This does not work for non-clausal formulas.
February 4, 2008.
Prover9. Minor bug: failed to renumber variables after one kind of
simplification (removing literal s!=t when s & t unify and do
not instantiate any other literal). This causes a problem
only when expanding a proof internally (e.g., newauto). Fixed.
January 29, 2008.
Directproof. Fix bug that caused it to fail if the unit
conflict involves a flip.
January 29, 2008.
Prover9/LADR. Change options processing a bit so that
options in the GUI make more sense. Introduce a new kind
of options dependency that resets options to defaults.
Several meta-options (lightest_first, breadth_first, random_given,
auto2, raw) did nothing when cleared. This is okay for
Prover9, but not for the GUI, which displays current values
of options.
-------- LADR Jan-2008 ---------- (unannounced release)
January 25, 2008.
Prover9. Two new flags for paramodulation: para_into_vars
(paramodulate into variables) and para_from_small (paramodulate
from smaller sides of oriented equalities). These are not
needed for finding refutations, but they can be useful for
*deriving* interesting things (fishing expeditions) and for
transforming a bidirectional proof into a forward proof.
Use with caution.
January 23, 2008.
Prooftrans. Some answer attributes were not being inherited
in translated proofs. Fixed by declaring answer attributes
to be inheritable.
-------- LADR Dec-2007 ----------
December 12, 2007.
Prover9. New flag "raw", which is a sort of anti-auto mode.
This removes restrictions on inference rules and other limits
on the search, allowing users to start from scratch and roll
their own strategies.
To see exactly what it does, set(raw) and look at the output.
December 9, 2007.
Mace4. New stringparm "iterate" takes values in
[all, evens, odds, primes, nonprimes]. "all" is default.
E.g., assign(iterate, odds).
This supersedes set(iterate_primes) and set(iterate_nonprimes),
and those two flags become meta-options which just assign
to "iterate".
December 5, 2007.
New program isofilter2, which uses a different
algorithm: canonicalize the interps so that isomorphic iff
identical. It also accepts a file of discriminators to
cut down the number of permutations. Results are mixed.
Isofilter (the original version). Add new option specifying
a file of discriminator clauses. Results are good.
Dprofile: new program to see how discriminators behave.
December 4, 2007.
Prover9. Allow restrict_denials to be used for non-Horn sets.
It usually doesn't make much sense for non-Horn sets (because
negative clauses usually don't correspond to the conclusion),
so let the user beware.
December 3, 2007.
Prooftrans. Get rid of multiple "Comments from original proof"
messages. These occurred when running prooftrans on the output
of a previous prooftrans job.
Prover9. New parm: assign(multiple_interps, false_in_some).
Default is false_in_all, which is the previous behavior.
If there are multiple interpretations, this parm determines
how a clause is labeled "false": false in some of the interps
or false in all of the interps.
Mace4. Bug calculating the maximum domain element in the
input: it was always >=0; it should be -1 when there are
none. This caused some extra isomorphic models to be
produced in some cases.
November 19, 2007.
Prover9. New parameter backsub_check (default 500) tells Prover9,
when it reaches the specified number of given clauses, to disable
back subsumption if the percentage of kept clauses that have been
back subsumed is less than 5%. Previously, this test was wired in
(at 500 given clauses), so behavior will be the same with the
default value.
ladr_to_tptp. Four changes:
(1) a <-> b translated correctly.
(2) Attributes on all formulas simply deleted.
(3) TPTP symbols that are different from the corresponding LADR
symbols (e..g, <=) can now be used as ordinary function or
predicate symbols in the LADR formulas; they are given new names.
(4) Clausal (CNF) goals are made into non-clausal (FOF) goals.
Isofilter. New command-line option "output" tells which operations
to output. Syntax is the same as the "check" option. Although
"check" and "output" will frequently be used together with
the same operations, e.g., isofilter check '*' output '*',
they are independent.
Also, change ignore_constants option so that constants are neither
checked nor output.
October 22, 2007.
Mace4. Undo the Oct 7 change to domain_size dependency, and
change how domain sizes are specified:
start_size (new parm, default 2)
end_size (new parm, default -1 (infinity))
domain_size (meta: copy value to start_size and end_size)
We'll keep iterate_up_to for a while, and make it a synonym
for end_size. That way, input (before Oct-2007) should behave
well. Note that that default end_size (iterate_up_to) is -1, not 10.
Mace4. New flag iterate_nonprimes (analogous to iterate_primes).
Mace4. There was an (arbitrary, I think) limit of 200 on the
domain size. I have removed this.
October 18, 2007.
Prover9. While working on adding the notion of dependent option to
the GUI, I decided that the dependent options in Prover9 should
be simplified. From now on, options that update other options
will be called meta options, and the only thing they do will be
to update other options (there might be a few exceptions).
The changes:
1. New flag auto_setup, whose role is to change eq_defs and
predicate_elim (previously controlled by auto_inference.
auto_setup is dependent on auto.
2. The back_unit_deletion flag has been removed. Now, there is
just 'unit_deletion', and back unit deletion is always done
when unit_deletion is set.
3. Back demodulation is set by default.
4. The flag positive_inference has been removed. (Positive
inference happens by default, because literal_selection is
max_negative by default.
LADR. New flag ignore_option_dependences. If set, dependencies
on options will be ignore during input. Dependencies will be
enabled after input, because options can change after input
(e.g., auto_inference, actions). This flag will be used by
the GUI, because the GUI will be handling dependencies.
-------- LADR Oct-2007 ----------
October 7, 2007.
Mace4. Remove option dependency:
domain_size=n -> iterate_up_to=0. Now, if you want to search
only one domain size, you'll have to assign to both domain_size
and iterate_up_to (to a value <= domain_size).
Prover9: Change literal_selection option value:
maximal_negative -> max_negative.
October 6, 2007.
Prooftrans and Interpformat: change exit codes. 0: at least one
proof/model processed. 2: no proof/model processed. 1: error.
October 4, 2007.
Prover9 and Mace4: new flag assign(report_stderr, <n>) sends "some"
statistics to stderr every n seconds and at the end.
This is for the GUI "Info" button.
October 3, 2007.
Interpformat: There is now a default format: "standard2".
(Previously a format had to be given.)
Mace4: Change flag names: print_models to print_models_tabular,
print_models_standard to print_models.
Mace4: Do not print === MODEL === for print_models_tabular,
because interpformat cannot handle it.
September 25, 2007.
Mace4: Change max_seconds and max_seconds_per so that -1
means infinity. (For consistency with Prover9 options.)
Update Mace4 HTML manual with these changes.
September 24, 2007.
LADR: Added primitive conditional inclusion for input.
The only conditions so far are "Prover9" and "Mace4".
if(Prover9). assign(max_given, 100). end_if.
if(Mace4). assign(domain_size, 5). end_if.
The conditions can be nested (though I don't see how that
would be useful so far).
September 18, 2007.
LADR: Change error messages for syntax errors and some other
input errors such as unrecognized options. Mark the beginning
of error as well as the end. This is so that errors can be
highlighted in the GUI. Also fix 2 parsing bugs: 'f(.' and '[.'
were crashing.
-------- LADR Aug-2007 ----------
August 3, 2007.
Interpformat, Mace4. Change the name of the interpretation format
"portable" to "standard". This is the format that LADR programs
use. This change was made so we could use "portable" for the
following.
Interpformat. Introduce a new output format "portable" to be used
for input to Python, GAP (and possibly Java and Javascript).
The new portable format is similar in structure to "standard",
but it is made up of natural numbers, double-quoted strings,
and lists. See the manual page "Interpformat".
July 18, 2007.
Prover9. Handling of redundant hints has been improved w.r.t.
labels and bsub_hint_wt attributes. Bsub_hint_wt attributes
on redundant (equivalent) hints are copied to the original (retained)
hint. If a hints ends up with more than one bsub_hint_wt
attribute, the first is used. When searching for matching
hints, if an equivalent hint is available, it is used; otherwise
the first subsumee is used.
June 30, 2007.
LADR. New language feature: allow the user to redefine several
built-in operations such as equality, disjunction, attribute.
For example,
redeclare(equality, "==").
redeclare(negated_equality, "=/=").
redeclare(disjunction, "&&").
The redeclarable operations are:
true, false, conjunction, disjunction, negation, implication,
backward_implication, equivalence, universal_quantification,
existential_quantification, attribute, equality, negated_equality.
Note: When a redeclaration occurs, the parsing/printing
properties (infix, precedence, etc.) are copied from the
old symbol to the new one.
June 18, 2007.
Prover9. New flag limit_hint_matchers (default clear). Setting
the flag causes max_{weight,literals,vars,depth} to be
applied to clauses that match hints.
-------- LADR June-2007 ----------
June 14, 2007.
LADR: Change printing of variables (standard style) to
x,y,z,u,w,v5,v6,v7,... . (That is, don't use "v".)
This avoids confusing terms like (v v v), because
"v" is commonly used as the lattice join operation.
June 13, 2007.
Prooftrans: fix the "proliferating ops problem", add option
striplabels, and append labels to hints only if asked to do so.
See the updated HTML manual.
June 12, 2007.
Prover9: Disabled rule pos_binary_resolution. The parameter
literal_selection (maximal_negative) will be used to do
positive binary resolution (and positive paramodulation).
The reason: before the change, we could have pos_binary_resolution
without positive paramodulation, which blocks proofs.
Change breadth_first "Starting on level" messages so they
don't appear if some other part has been set.
June 4, 2007.
Newauto, newsax, autosketches (non-documented experimental
programs): updates for expand_relational_defs broke these
programs. Fixed by including call to embed_formulas_in_topforms.
-------- LADR May-2007 ----------
May 21-23, 2007.
Prover9: Added flag set(expand_relational_defs) (default clear),
which causes Prover9 to look for relational definitions in
the assumptions, and use them to expand all occurrences
of the defined relation in the input, before the start of
the search. See the HTML manual, page "More Prep".
May 6-11, 2007.
Prover9: *MAJOR* changes to binary resolution and paramodulation
for non-unit clauses. The goal is improved performance
for non-unit, especially non-Horn, problems.
There are several changes in flags and parameters.
See the Prover9 HTML manual page "Inference Rules".
An unfortunate consequence of these changes is that
paramodulation for (unit) equational problems can
behave differently from previous versions, because
paramodulants can be derived in a different order,
causing given clauses to be selected in a different order.
May 9, 2007.
Change default predicate symbol precedence so that equality
is the smallest instead of the largest. In problems with
both equality and non-equality predicates, this change
usually causes resolution to occur before paramodulation.
May 8, 2007.
Separate the lex([...]) command into two commands:
function_order([...]) and predicate_order([...]).
(The old lex([...]) command will continue to be accepted,
and it is now a synonym for function_order([...]).)
May 8, 2007.
Bob Veroff reminded me that the parsing code can
accept ambiguous terms, for example, if ~ is prefix and '
is postfix with the same precedence, the term (~ x ') is
accepted. (Prolog systems (all Prologs??) have the same
problem.) Fix: do not allow declarations of two different
symbols with different parse types and the same precedence.
This applies also to built-in declarations, so the error may
be confusing. Also change built-in precedence of
op(400, prefix, -) to op(350, prefix, -), because people tend
to use 400 for infix ops.
April 19, 2007.
Prover9, minor bug: If predicates were eliminated in preprocessing,
they were still listed in the symbol precedence for the search
(at the top of the order). Fixed.
April 18-19, 2007.
Ken Kunen reminded me that Prover9 doesn't paramodulate from
variables, making it incomplete when there are (positive)
equality literals t=x in which variable x does not occur in term t.
A new flag: para_from_vars (default set). Note that this is almost
always irrelevant for purely equational (unit) problems.
April 16, 2007.
prooftrans: bug reading proofs containing justifications
with more than 256 rewrites. There is a hard limit of 256
on the arity of symbols. Fix: change format of rewrite
justifications from "rewrite(step1,step2, ...)" to
"rewrite([step1,step2, ...])". After the fix, you can use
the new prooftrans prooftrans only with new prover9 outputs,
and old prooftrans only with old prover9 outputs.
Related: check for arity-too-big when building terms.
April 16, 2007.
LADR: yet another parsing bug. Terms like "h(v) * (x + y)"
(assuming v is infix (the default)) are parsed incorrectly
(parser thinks v is binary and * is unary. Fixed.
-------- LADR April-2007 ----------
April 12, 2007.
Mace4: fixed 2 bugs in signal handling.
Apps.src: updated clausefilter, clausetester, interpfilter so that
they work for non-clausal formulas as well as clauses.
April 9, 2007.
Prooftrans bug: fatal error expanding new_constant inference
with secondary justification. Fixed.
April 6, 2007.
Prover9, added parm var_penalty, which can be used to penalize
clauses by the number of (distinct) variables. At the end of
the weighing process, the weight is increased by
n * number_of_variables. N can be negative, which lowers the
weight. Update manual.
April 5, 2007.
Prover9, Bugs: max_depth, max_vars, max_literals can delete
clauses that match hints. Also, sos_keep can delete clauses
that match hints. These were fixed by reorganizing the
cl_process_delete code.
April 3, 2007.
Isofilter: very slow memory leak. Fixed (zap_interp failed
to free comments).
April 2, 2007.
Prover9, new flags and parms for selecting the given clause:
parm random_part: picks random clauses from sos;
flag random_given: random_part=1, other parts (except hints) 0;
parm random_seed: (-1 means use "random seed");
flag default_parts: clearing sets ALL parts to 0.
-------- LADR March-2007 ----------
March 16, 2007.
Two new utilities to support the TPTP language:
ladr_to_tptp: Prover9 input file -> TPTP problem file.
tptp_to_ladr: TPTP problem file -> Prover9/Mace4 formulas.
These are still in development and do not yet support all
of the TPTP features. Eventually, Prover9 and Mace4 will
accept the TPTP language directly.
March 15, 2007.
Prover9: insert several fflush() so that output is better
behaved when stderr is sent to the same file as stdout.
March 12, 2007.
Prover9: new parms max_depth and depth_penalty.
Prover9: new command-line option -p causes all output to
be fully parenthesized. This is mostly to check and debug
parsing declarations (op commands).
March 7, 2007.
LADR: Bug in clausify_prepare causes result of Skolemization to be
more complex than necessary. Fixed.
Prover9: max_megs limit caused fatal error if it occurred in
CNF translation (before search). Fixed.
LADR: Several substantial changes to basic parsing of terms:
1. Previously, some legal terms were rejected. For example,
if you have a binary infix op, say *, and you use it as a
unary op, and write it in standard form, say p(*(x)), it
would be rejected. (Input cannot have a symbol with multiple
arities, but if it is declared, but not used, that does not
count.) Several cases like this have been fixed, but there
may still be related problems.
2. Parsing/printing of quantified formulas has been changed.
Previously, "p | all x q | r" would be rejected. Now
it is accepted with association "p | (all x q) | r".
Also, fewer parentheses are output for quantified formulas.
Quantifiers have lower precedence (bind tighter) than other
logic operations, so "all x p -> q" means "(all x p) -> q".
When in doubt, include parentheses and look at the output.
March 5, 2007.
Bug in manual (Clauses and Formulas section): the "cons"
operator is shown as "|" (as in Prolog), but it is really ":".
Fixed.
February 27, 2007.
Prooftrans (from Kinyon): bug with options "expand renumber".
The transformed proof can have strage IDs, e.g., 27A. Fixed.
February 12, 2007.
Prover9 bug: KBO and fold_eq, in a problem with exactly one unary
operation, that happens to be an equational definition. Fold_eq
can arrange the precedence in a way that violates the KBO rules,
causing non-termination. Fix: do not change precedence of
special unary op (such symbol is still folded).
January 30, 2007
Updated the Mace4 pages of the (HTML) Prover9 Manual. Previously
the Mace4 pages were cursory, with reference to the out-of-date
(2003) tech memo. Now the HTML version is reasonably complete.
January 26, 2007
Hints are now back demodulated (as in Otter).
January 22-25, 2007
Prover9: Major overhaul of the given clause selection code.
A new source file prover9.src/picker.c was introduced;
the files ladr/sos.c and prover9.src/control_sos.c are now gone.
BEWARE: YOU WILL NOTICE A DIFFERENCE. Even with the same input,
given clauses will probably be selected in a different order from
previous versions, resulting in different searches. There is
no way to opt for the old method.
The main difference has to do with the selection ratio. Previously,
if a clause of a particular type was not available, another
type could be substituted. Now, if none is available, that type
is skipped. Because of this change, the default values of
true_part and false_part have been changed from 2 to 4.
Also, there is a new parameter "weight_part", which is used
for basic selection-by-weight. (Previously, true_part and
false_part were used in a round-about way for simple
selection-by-eight.) There is a new (meta-)flag "lightest_first",
which sets weight_part=1 and all other parts to 0 (except hints_part).
Also, "pick_given_ratio" now sets weight_part=n, age_part=1,
true_part=false_part=0.
Selection by Hints: Previously clauses that matched hints
were given preference simply by adjusting their weights.
Now, clauses that match hints have their own component of the
selection ratio: "hints_part", with default value infinity,
and those clauses now get ordinary weights.
In summary, the components of the selection ratio are (with defaults):
age_part 1
true_part 4
false_part 4
weight_part 0
hints_part INT_MAX
Other "_part"s may be added in the future.
The manual has been updated to reflect all of these changes.
January 24, 2007
Prover9 bug: answer attributes not instantiated for the "xx"
(resolve with x=x) simplification rule. The first version of
this rule simply removed instances of x!=x, so answer attributes
didn't have to be instantiated. However, the rule was changed
so that it removes s!=t, when s and t are unifiable without
instantiating any other literals in the clause. When I made
the change, I overlooked the fact that it can instantiate
answer attributes. Fixed.
--------- LADR-Jan-2007 ----------
January 4, 2007
December 11, 2006
Isofilter: A new option to specify exactly the symbols to be
used for the isomorphism checks. (Sort of a generalization of
"ignore_constants".) It is given on the command line, e.g.,
the command "isofilter check '+ *'" says to consider only those
two operations (any other operations are still printed in the
results). If there is more than one operation, or if some of
the operations might be interpreted by the shell, include
single quotes as in the example. This was prompted by
Joao Araujo.
December 8, 2006
Improve warning messages for symbols missing from lex command
and extra symbols in lex command.
December 5, 2006
Prover9 (bug reported by Sebastian Sonntag): Predicate elimination
changes the basic clause properties so auto_denials gets the
wrong count of number of negative clauses. Fix: move
basic_clause_properties() after predicate elimination.
December 3, 2006
Prooftrans: change heading on "prooftrans ivy" output.
--------- LADR-November-2006 ----------
November 22, 2006