Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP Path: utzoo!utgpu!water!watnot!watmath!clyde!cbatt!ihnp4!inuxc!pur-ee!uiucdcs!uiucdcsb!kadie From: kadie@uiucdcsb.UUCP Newsgroups: comp.ai Subject: Re: AI Project Information Request Message-ID: <165000002@uiucdcsb> Date: Sun, 29-Mar-87 19:24:00 EST Article-I.D.: uiucdcsb.165000002 Posted: Sun Mar 29 19:24:00 1987 Date-Received: Tue, 31-Mar-87 05:15:31 EST References: <410@qiclab.UUCP> Lines: 208 Nf-ID: #R:qiclab.UUCP:410:uiucdcsb:165000002:000:7971 Nf-From: uiucdcsb.cs.uiuc.edu!kadie Mar 29 18:24:00 1987 Several people have ask if the grammar checker I used was real. It is. It is a commercial product for the IBM PC. Here is some more information and an example. I own a spelling checker that I always use. And a grammar and style checker that I sometimes use. I have a lot of confidence in the spelling checker; I take virtually all of its advice. The style checker is not as good. I always consider it's suggestions, but I know that it has missed many grammar and style errors and that not everything it flags is really wrong. Enclosed find its critique of a draft report. This gives a pretty good indication of how well the program works. The program is RIGHTWRITER version 2.0, a Right Soft product by Decisionware, Inc. of 2033 Wood Street, Suite 218, Sarasota, Florida 33577. It runs on IBM PC's and compatible computers. It costs about $100.00. Carl Kadie University of Illinois at Urbana-Champaign UUCP: {ihnp4,pur-ee,convex}!uiucdcs!kadie CSNET: kadie@UIUC.CSNET ARPA: kadie@M.CS.UIUC.EDU (kadie@UIUC.ARPA) (I disclaim any ulterior relationship to Decisionware.) ------------------------------- .+c "A Program To Compute Moore's Stable Expansions" .pp Moore has recently proposed a possible-world semantics for autoepistemic logic. His method has the intriguing property of producing multiple expansions, that <<* 16. UNNECESSARY COMMA *>>^ is it list the (finite) theories of what you believe about the world, given the axioms. ^<<* 17. LONG SENTENCE: 27 WORDS *>> For example, if your unbelief in proposition $P$ implies $Q$, and your unbelief in proposition $Q$ implies $P$, then we can theorize that either $P$ is true or alternatively $Q$ true. <<* 17. LONG SENTENCE: 31 WORDS *>>^ <<* 31. COMPLEX SENTENCE *>>^ .pp In Lisp notation the axioms are expressed: .(L (and (imp (not (l 'p)) q) (imp (not (l 'q)) p)) .)L and the conclusion is expressed: .(L (Q) (P) .)L .pp I have written a program that finds the stable expansions of formula in Moore's autoepistemic logic. As might be expected <<* 21. PASSIVE VOICE: be expected *>>^ the program run in time exponential to the number of variables. <<* 32. INCOMPLETE SENTENCE OR MISSING COMMA *>>^ Let's look at some runs: .(L A non-autoepistemic sentence: (expand '(and p (imp p (not q)) (imp (not q) r)) ;; axioms '(p q r) ;; propositions 0) ;; trace level returns: ((P (NOT Q) R)) .)L In other words, the axioms entail that $P$ is true, $Q$ is false, and $R$ is true. This is of course just what we expect for this propositional sentence. .pp Here is a trace of the run of the example we saw before: .(L [Figure goes here. -- CMK] .)L .pp The program also identifies cases where no stable expansion exists: .(L [Figure goes here. -- CMK] .)L .pp At higher trace levels, the program provides counter-models to non-grounded theories. For example: .(L (expand '(and (imp (not (l 'p1)) p2) (imp (not (l 'p2)) p3) (imp (not (l 'p3)) p4) (imp (not (l 'p4)) p1)) '(p1 p2 p3 p4) 2) ... (P1 P2 P3 P4) in theory is stable w.r.t. the axioms. S5 is ((P1 P2 P3 P4)) (s5:((P1 P2 P3 P4)) , V:((NOT P1) P2 (NOT P3) P4)) is a model of A Counter-model: (s5:((P1 P2 P3 P4)), V:((NOT P1) P2 (NOT P3) P4)) Theory (P1 P2 P3 P4) is NOT a stable expansion of the axioms ... ((P2 P4) (P1 P3)) .)L .pp In fact it is just this test of groundness that makes Moore's logic different from the logic of Shoham that we will see later. <<* 17. LONG SENTENCE: 24 WORDS *>>^ For example when we give Shoham's gun example to the program it replies that there are no stable <<* 1. REPLACE: that there BY there *>>^ expansions. This is because it does not have Shoham's chronological ignorance criteria with which to choose ungrounded theories. Here is the trace: .(L [Figure goes here. -- CMK] .)L .pp Having no stable expansion and believing nothing are two separate case. Here is a case where the only stable expansion is the theory where nothing is believed. ^<<* 21. PASSIVE VOICE: is believed. *>> .(L [Figure goes here. -- CMK] .)L .pp The program works by enumerating every theory, then constructing the corresponding S5 structure. Next, it tests every world of the S5, if any world fails to support the axioms then it is unstable and the theory is removed from consideration. <<* 21. PASSIVE VOICE: is removed *>>^ <<* 17. LONG SENTENCE: 27 WORDS *>>^ Stable theories are next tested for groundness. This is done <<* 21. PASSIVE VOICE: are next tested *>> <<* 21. PASSIVE VOICE: is done *>>^ by trying every variable assignment $V$. If an assignment makes the axioms true then $V$ must correspond to a world in the S5, or else the theory is not grounded. A theory <<* 21. PASSIVE VOICE: is not grounded. *>>^ <<* 17. LONG SENTENCE: 33 WORDS *>>^ that is both stable and grounded is added to the stable <<* 21. PASSIVE VOICE: is added *>>^ expansion list to be returned at the end of the program. <<* 21. PASSIVE VOICE: be returned *>> <<* 17. LONG SENTENCE: 24 WORDS *>>^ .pp Overall, the program works very well on small problems (four variable problems take only seconds on a SUN). The program accepts any formula that Lisp can evaluate; so very complex formula may be input. However, since the program relies on enumeration, it can not be expanded <<* 21. PASSIVE VOICE: be expanded *>>^ to first-order logic, nor can it be considered practical <<* 21. PASSIVE VOICE: be considered *>>^ unless the problems can be guaranteed to be small. <<* 21. PASSIVE VOICE: be guaranteed *>> <<* 17. LONG SENTENCE: 31 WORDS *>>^ <<* 31. COMPLEX SENTENCE *>>^ <<** SUMMARY **>> READABILITY INDEX: 7.63 Readers need an 8th grade level of education to understand. STRENGTH INDEX: 0.19 The writing can be made more direct by using: - the active voice - shorter sentences - more common words - fewer abbreviations DESCRIPTIVE INDEX: 0.74 The use of adjectives and adverbs is within the normal range. JARGON INDEX: 0.25 SENTENCE STRUCTURE RECOMMENDATIONS: 15. No Recommendations. << UNCOMMON WORD LIST >> The following words are not widely understood. Will any of these words confuse the intended audience? AUTOEPISTEMIC 3 AXIOM 2 AXIOMS 40 CHRONOLOGICAL 1 CRITERIA 1 DRIBBLE 1 ENTAIL 1 ENUMERATING 1 ENUMERATION 1 EXPONENTIAL 1 FINITE 1 FIRE4 20 GROUNDNESS 2 IMP 24 INTRIGUING 1 LISP 2 LOAD1 20 MOORE 1 MOORE'S 3 NIL 5 NOISE6 17 P 4 PROPOSITION 2 PROPOSITIONAL 1 PROPOSITIONS 2 Q 4 R 1 SEMANTICS 1 SHOHAM 1 SHOHAM'S 2 THEORIZE 1 UNBELIEF 2 UNGROUNDED 1 V 2 VACUUM5 17 WRT 19 << END OF UNCOMMON WORD LIST >> <<** WORD FREQUENCY LIST **>> A 31 ABOUT 1 ACCEPTS 1 ADD 1 ALSO 1 ALTERNATIVELY 1 AN 1 AND 18 ANY 2 ARE 4 AS 1 ASSIGNMENT 3 AT 3 AUTOEPISTEMIC 3 AXIOM 2 AXIOMS 40 BE 7 BECAUSE 1 BEFORE 1 BELIEVE 3 BOTH 1 [Rest of word frequency list goes here -- CMK] <>