miller:examples/ljfol >~/terzo/bin/Terzo loading /share/pub/miller/terzo/bin/.lpsml ......................... done Terzo lambda-Prolog, Version 1.0b, Built Tue Jul 16 15:52:11 EDT 1996 [reading file /share/pub/miller/terzo/lib/terzo.rc] [closed file /share/pub/miller/terzo/lib/terzo.rc] Terzo> #load "go". [reading file ./go] [reading file /share/pub/miller/terzo/doc/SystemModules/maps.mod] module maps [closed file /share/pub/miller/terzo/doc/SystemModules/maps.mod] [reading file /share/pub/miller/terzo/lib/list_util.mod] module ListUtil [closed file /share/pub/miller/terzo/lib/list_util.mod] [reading file /share/pub/miller/elios/lProlog/examples/utilities/control.mod] module control [closed file /share/pub/miller/elios/lProlog/examples/utilities/control.mod] [reading file /share/pub/miller/elios/lProlog/examples/utilities/lists.mod] module lists [closed file /share/pub/miller/elios/lProlog/examples/utilities/lists.mod] [reading file /share/pub/miller/elios/lProlog/examples/utilities/alist.mod] module Alist [closed file /share/pub/miller/elios/lProlog/examples/utilities/alist.mod] [reading file /share/pub/miller/elios/lProlog/examples/tactics/goals.mod] module goals [closed file /share/pub/miller/elios/lProlog/examples/tactics/goals.mod] [reading file /share/pub/miller/elios/lProlog/examples/tactics/goalred.mod] module goalred [closed file /share/pub/miller/elios/lProlog/examples/tactics/goalred.mod] [reading file /share/pub/miller/elios/lProlog/examples/tactics/maptac.mod] module maptac [closed file /share/pub/miller/elios/lProlog/examples/tactics/maptac.mod] [reading file /share/pub/miller/elios/lProlog/examples/tactics/tacticals.mod] module tacticals [closed file /share/pub/miller/elios/lProlog/examples/tactics/tacticals.mod] [reading file /share/pub/miller/elios/lProlog/examples/tactics/inter_tacs.mod] module inter_tacs [closed file /share/pub/miller/elios/lProlog/examples/tactics/inter_tacs.mod] [reading file /share/pub/miller/elios/lProlog/examples/ljfol/fol.mod] module fol [closed file /share/pub/miller/elios/lProlog/examples/ljfol/fol.mod] [reading file /share/pub/miller/elios/lProlog/examples/ljfol/printer.mod] module printer [closed file /share/pub/miller/elios/lProlog/examples/ljfol/printer.mod] [reading file /share/pub/miller/elios/lProlog/examples/ljfol/scanner.mod] module scanner [closed file /share/pub/miller/elios/lProlog/examples/ljfol/scanner.mod] [reading file /share/pub/miller/elios/lProlog/examples/ljfol/parser.mod] module parser [closed file /share/pub/miller/elios/lProlog/examples/ljfol/parser.mod] [reading file /share/pub/miller/elios/lProlog/examples/ljfol/formulas.mod] module formulas [closed file /share/pub/miller/elios/lProlog/examples/ljfol/formulas.mod] [reading file /share/pub/miller/elios/lProlog/examples/ljfol/lj.mod] module lj [closed file /share/pub/miller/elios/lProlog/examples/ljfol/lj.mod] [reading file /share/pub/miller/elios/lProlog/examples/ljfol/rules.mod] module rules [closed file /share/pub/miller/elios/lProlog/examples/ljfol/rules.mod] [reading file /share/pub/miller/elios/lProlog/examples/ljfol/top.mod] module top [closed file /share/pub/miller/elios/lProlog/examples/ljfol/top.mod] [closed file ./go] Terzo> #query top prover. The following formulas are available for proving: distrib_quant1 distrib_quant2 distrib_quant3 cases1 cases2 cases3 bugs blocks baffler modus_quant primes reflexive quant_equiv Enter a formula name: blocks. ----------------------------------- (((((((forall x ((blue x) => (neg (green x)))) and (blue c)) and (green a)) and (on_top b c)) and (on_top a b)) and (forall x ((neg (green x)) or (green x)))) => (exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y))))) Enter tactic: go. (1) (forall x ((blue x) => (neg (green x)))) (2) (blue c) (3) (green a) (4) (on_top b c) (5) (on_top a b) (6) (forall x ((neg (green x)) or (green x))) ----------------------------------- (exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y)))) Enter tactic: forallq_l 6. Enter term: b. (1) ((neg (green b)) or (green b)) (2) (forall x ((blue x) => (neg (green x)))) (3) (blue c) (4) (green a) (5) (on_top b c) (6) (on_top a b) (7) (forall x ((neg (green x)) or (green x))) ----------------------------------- (exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y)))) Enter tactic: weaken 7. (1) ((neg (green b)) or (green b)) (2) (forall x ((blue x) => (neg (green x)))) (3) (blue c) (4) (green a) (5) (on_top b c) (6) (on_top a b) ----------------------------------- (exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y)))) Enter tactic: or_l 1. (1) (neg (green b)) (2) (forall x ((blue x) => (neg (green x)))) (3) (blue c) (4) (green a) (5) (on_top b c) (6) (on_top a b) ----------------------------------- (exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y)))) Enter tactic: existsq_r. Enter term: a. (1) (neg (green b)) (2) (forall x ((blue x) => (neg (green x)))) (3) (blue c) (4) (green a) (5) (on_top b c) (6) (on_top a b) ----------------------------------- (exists y (((on_top a y) and (neg (green y))) and (green a))) Enter tactic: existsq_r. Enter term: b. (1) (neg (green b)) (2) (forall x ((blue x) => (neg (green x)))) (3) (blue c) (4) (green a) (5) (on_top b c) (6) (on_top a b) ----------------------------------- (((on_top a b) and (neg (green b))) and (green a)) Enter tactic: go. (1) (green b) (2) (forall x ((blue x) => (neg (green x)))) (3) (blue c) (4) (green a) (5) (on_top b c) (6) (on_top a b) ----------------------------------- (exists y (exists y1 (((on_top y y1) and (neg (green y1))) and (green y)))) Enter tactic: existsq_r. Enter term: b. (1) (green b) (2) (forall x ((blue x) => (neg (green x)))) (3) (blue c) (4) (green a) (5) (on_top b c) (6) (on_top a b) ----------------------------------- (exists y (((on_top b y) and (neg (green y))) and (green b))) Enter tactic: existsq_r. Enter term: c. (1) (green b) (2) (forall x ((blue x) => (neg (green x)))) (3) (blue c) (4) (green a) (5) (on_top b c) (6) (on_top a b) ----------------------------------- (((on_top b c) and (neg (green c))) and (green b)) Enter tactic: go. (1) (green c) (2) (green b) (3) (forall x ((blue x) => (neg (green x)))) (4) (blue c) (5) (green a) (6) (on_top b c) (7) (on_top a b) ----------------------------------- false Enter tactic: forallq_l 3. Enter term: 4. Tactic failed. (1) (green c) (2) (green b) (3) (forall x ((blue x) => (neg (green x)))) (4) (blue c) (5) (green a) (6) (on_top b c) (7) (on_top a b) ----------------------------------- false Enter tactic: forallq_l 3. Enter term: c. (1) ((blue c) => (neg (green c))) (2) (green c) (3) (green b) (4) (forall x ((blue x) => (neg (green x)))) (5) (blue c) (6) (green a) (7) (on_top b c) (8) (on_top a b) ----------------------------------- false Enter tactic: imp_l 1. (1) ((blue c) => (neg (green c))) (2) (green c) (3) (green b) (4) (forall x ((blue x) => (neg (green x)))) (5) (blue c) (6) (green a) (7) (on_top b c) (8) (on_top a b) ----------------------------------- (blue c) Enter tactic: go. (1) (neg (green c)) (2) (green c) (3) (green b) (4) (forall x ((blue x) => (neg (green x)))) (5) (blue c) (6) (green a) (7) (on_top b c) (8) (on_top a b) ----------------------------------- false Enter tactic: neg_l 1. (1) (neg (green c)) (2) (green c) (3) (green b) (4) (forall x ((blue x) => (neg (green x)))) (5) (blue c) (6) (green a) (7) (on_top b c) (8) (on_top a b) ----------------------------------- (green c) Enter tactic: go. solved Terzo>