Script started on Wed Apr 23 11:17:55 2003 adara/563> mlisp International Allegro CL Enterprise Edition 6.2 [Solaris] (Jun 26, 2002 11:20) Copyright (C) 1985-2002, Franz Inc., Berkeley, CA, USA. All Rights Reserved. This development copy of Allegro CL is licensed to: [4549] SUNY/Buffalo, N. Campus ;; Optimization settings: safety 1, space 1, speed 1, debug 2. ;; For a complete description of all compiler switches ;; given the current optimization settings evaluate ;; (explain-compiler-settings). ;;--- ;; Current reader case mode: :case-sensitive-lower cl-user(1): :ld /projects/snwiz/bin/sneps ; Loading /projects/snwiz/bin/sneps.lisp Loading system SNePS...10% 20% 30% 40% 50% 60% 70% 80% 90% 100% SNePS-2.6 [PL:0a 2002/09/30 22:37:46] loaded. Type `(sneps)' or `(snepslog)' to get started. cl-user(2): (snepslog) Welcome to SNePSLOG (A logic interface to SNePS) Copyright (C) 1984--2002 by Research Foundation of State University of New York. SNePS comes with ABSOLUTELY NO WARRANTY! Type `copyright' for detailed copyright information. Type `demo' for a list of example applications. : demo "pegasus-full.snlog" av File /web/faculty/rapaport/563/pegasus-full.snlog is now the source of input. The demo will pause between commands, at that time press RETURN to continue, or ? to see a list of available commands : ;; Simple demo that shows how SNePSLOG handles ;; contradictions: clearkb Knowledge Base Cleared : ;; Tornado is a white horse white(tornado) --- pause --- white(tornado) CPU time : 0.01 : horse(tornado) --- pause --- horse(tornado) CPU time : 0.00 : ;; Horses do not fly all (x) (horse(x) => ~flies(x)) --- pause --- all(x)(horse(x) => (~flies(x))) CPU time : 0.01 : ;; Winged horses do fly... all (x) (winged-horse(x) => flies(x)) --- pause --- all(x)(winged-horse(x) => flies(x)) CPU time : 0.00 : ;; ...they are horses... all (x) (winged-horse(x) => horse(x)) --- pause --- all(x)(winged-horse(x) => horse(x)) CPU time : 0.00 : ;; ... and they have wings. all (x) (winged-horse(x) => has-wings (x)) --- pause --- all(x)(winged-horse(x) => has-wings(x)) CPU time : 0.00 : ;; Pegasus is a winged horse winged-horse(pegasus) --- pause --- winged-horse(pegasus) CPU time : 0.00 : ;; Does Pegasus have wings...YES has-wings(pegasus)? --- pause --- I wonder if has-wings(pegasus) holds within the BS defined by context default-defaultct I wonder if winged-horse(pegasus) holds within the BS defined by context default-defaultct I know winged-horse(pegasus) Since all(x)(winged-horse(x) => has-wings(x)) and winged-horse(pegasus) I infer has-wings(pegasus) has-wings(pegasus) CPU time : 0.02 : ;; Does Tornado fly? - NO flies(tornado)? --- pause --- I wonder if flies(tornado) holds within the BS defined by context default-defaultct I wonder if winged-horse(tornado) holds within the BS defined by context default-defaultct I wonder if horse(tornado) holds within the BS defined by context default-defaultct I know horse(tornado) Since all(x)(horse(x) => (~flies(x))) and horse(tornado) I infer ~flies(tornado) I know it is not the case that flies(tornado) ~flies(tornado) CPU time : 0.11 : ;; Does Pegasus fly? Type in the query and try it out. flies(pegasus)? --- pause --- I wonder if flies(pegasus) holds within the BS defined by context default-defaultct I wonder if winged-horse(pegasus) holds within the BS defined by context default-defaultct I wonder if horse(pegasus) holds within the BS defined by context default-defaultct I know winged-horse(pegasus) Since all(x)(winged-horse(x) => flies(x)) and winged-horse(pegasus) I infer flies(pegasus) I wonder if winged-horse(pegasus) holds within the BS defined by context default-defaultct I know winged-horse(pegasus) Since all(x)(winged-horse(x) => horse(x)) and winged-horse(pegasus) I infer horse(pegasus) Since all(x)(horse(x) => (~flies(x))) and horse(pegasus) I infer ~flies(pegasus) The contradiction involves the newly derived proposition: ~flies(pegasus) and the previously existing proposition: flies(pegasus) A contradiction was detected within context default-defaultct. You have the following options: 1. [C]ontinue anyway, knowing that a contradiction is derivable; 2. [R]e-start the exact same run in a different context which is not inconsistent; 3. [D]rop the run altogether. (please type c, r or d) =><= r In order to make the context consistent you must delete at least one hypothesis from each of the following sets of hypotheses: (wff7 wff5 wff4 wff3) WARNING: the following hypothesis supports BOTH contradictory WFFS, so removing it might be too extreme a revision. winged-horse(pegasus) In order to make the context consistent you must delete at least one hypothesis from the set listed below. An inconsistent set of hypotheses: 1 : winged-horse(pegasus) (5 supported propositions: (wff14 wff13 wff12 wff8 wff7) ) 2 : all(x)(winged-horse(x) => horse(x)) (3 supported propositions: (wff14 wff13 wff5) ) 3 : all(x)(winged-horse(x) => flies(x)) (2 supported propositions: (wff12 wff4) ) 4 : all(x)(horse(x) => (~flies(x))) (3 supported propositions: (wff14 wff11 wff3) ) Enter the list number of a hypothesis to examine or [d] to discard some hypothesis from this list, [a] to see ALL the hypotheses in the full context, [r] to see what you have already removed, [q] to quit revising this set, or [i] for instructions (please type a number OR d, a, r, q or i) =><= 2 all(x)(winged-horse(x) => horse(x)) WFFS that depend on wff5: ~flies(pegasus) horse(pegasus) all(x)(winged-horse(x) => horse(x)) What do you want to do with hypothesis wff5? [d]iscard from the context, [k]eep in the context, [u]ndecided, [q]uit revising this set, [i]nstructions (please type d, k, u, q or i) =><= d The consistent set of hypotheses: 1 : winged-horse(pegasus) (5 supported propositions: (wff14 wff13 wff12 wff8 wff7) ) 2 : all(x)(winged-horse(x) => flies(x)) (2 supported propositions: (wff12 wff4) ) 3 : all(x)(horse(x) => (~flies(x))) (3 supported propositions: (wff14 wff11 wff3) ) Enter the list number of a hypothesis to examine or [d] to discard some hypothesis from this list, [a] to see ALL the hypotheses in the full context, [r] to see what you have already removed, [q] to quit revising this set, or [i] for instructions (please type a number OR d, a, r, q or i) =><= q The following (not known to be inconsistent) set of hypotheses was also part of the context where the contradiction was derived: (wff6 wff2 wff1) Do you want to inspect or discard some of them? =><= n Do you want to add a new hypothesis? =><= n I know flies(pegasus) flies(pegasus) CPU time : 0.21 : list-asserted-wffs ~(all(x)(winged-horse(x) => horse(x))) flies(pegasus) ~flies(tornado) has-wings(pegasus) winged-horse(pegasus) all(x)(winged-horse(x) => has-wings(x)) all(x)(winged-horse(x) => flies(x)) all(x)(horse(x) => (~flies(x))) horse(tornado) white(tornado) : End of /web/faculty/rapaport/563/pegasus-full.snlog demonstration. CPU time : 0.89 : lisp Bye nil cl-user(3): (exit) ; Exiting Lisp adara/563> exit exit script done on Wed Apr 23 11:19:08 2003