SCREEN 1. MODAL LOGIC THEORY
FOR PATHOLOGY INFERENCE.
G. William Moore, MD, PhD.
Lawrence A. Brown, MD.
Robert H. Burger, MD, MPA.
Grover M. Hutchins, MD.
Robert E. Miller, MD.
http://www.medparse.com/modlthry.htm

From the Pathology and Laboratory Medicine Service, Baltimore Veterans Affairs Maryland Health Care System; and Departments of Pathology, University of Maryland Medical System and The Johns Hopkins Medical Institutions, Baltimore, MD.
Presented: Thursday, September 25, 2003, meeting, Biomedical Computing Interest Group (BCIG), U. S. National Institutes of Health, Clinical Center, 1:00 to 3:00 PM. For additional notes and references, see: http://www.netautopsy.org/modlnote.htm

U. S. Government Work, uncopyrighted, submitted for publication to:
Becich MJ, Crowley R, course directors.
Advancing Practice, Instruction, and Innovation through Informatics. Frontiers in Oncology and pathology. Eighth Annual Conference.
Pittsburgh, PA: University of Pittsburgh Medical Center. October 8-10, 2003. 2003;:.
http://apiii.upmc.edu

SCREEN 2. ABSTRACT.

Pathology studies the etiology and pathogenesis of disease. Anatomic pathology is devoted to the gross anatomy and microanatomy of diseased organs, aimed at rendering specific diagnoses, and acquiring new knowledge about disease biology. A major function of the anatomic pathologist is to issue diagnostic reports on samples from diseased tissue. The aggregate collection of reports contains a wealth of information related to almost every serious human disease.

Any data-mining program must incorporate the fundamental constraints on data acquisition in routine medical practice. It may be unnecessary, uneconomic, technically unfeasible, or unethical to fill in all possible data-items in a rectangular database. Existing clinical databases should include formal considerations for missing values, patient consent, patient risk, and provider alerts. This report proposes a mathematically consistent theory of clinicopathologic inference with the modal concepts of know-whether ($), need-to-know-whether (#), and try-to-know-whether (!).

The theory employs the ATOMSET of distinct, atomic statements (atoms, A), each of which has a definite true-false status (no self-reference paradoxes). Quantitative, interval, ranked, and categorical data are reformulated as true-false statements. Each atom is either a datum (complaints, history, physical findings, laboratory values, statements of consent, etc.); or a medical entity (cancer, inflammation, necrosis, etc.). No datum is an entity and no entity is a datum. To each atom, a in set A, denoted a C A, there exists known-to-the-k-a, $ka in set $A, denoted $ka C $A, for every integer k up to a maximum, M; and additionally for each datum, d in set D, denoted d C D, there is need-to-know-d, #d in set #D, denoted #d C #D, and try-to-know-d, !d in set !D, denoted !d C !D. A datum is d-Hippocratic (do-no-harm) if and only if (not-#d implies not-!d); and d-conative (try) if and only if ((not-$d and #d) implies !d). An entity may be keð..d-vexative (worrisome) kðe-ontologic (exists), based upon previously collected data.

The theory is mathematically consistent, and satisfies Occam's Razor, namely, that no entities are known without data. The d-Hippocratic, d-conative, keð..d-vexative, and kðe-ontologic properties are consistent if data are entered consensually, consecutively, and consistently, i.e., no datum is entered after its negation has been entered. The computer algorithm concludes within polynomial time. This report introduces a mathematical system for managing medical concepts and data. Modal logic operators expand the purview of classical symbolic logic, to accommodate technical, economic, and consent-based constraints on clinicopathologic data collection. The theory supports such medical concepts as: do-no-harm; try-if-you-need-to; worrisome findings; disease ontologies; and levels of certainty.

The theory is completely general, and permits definitions of patient injury that include possible death, morbidity, inconvenience, financial constraints, or loss-of-privacy; and definitions of need-to-know that may differ among observers (patient, physician, insurer, national health policy, research protocol).

Mathematical theories can serve to organize medical knowledge and patient data, and improve the scheduling and effectiveness of data collection and surveillance in large clinicopathologic data systems.

SCREEN 3. TABLE OF CONTENTS.


1. Title Page.
2. Abstract.
3. Table of Contents.
4. Introduction.
5. Hypothetical Autopsy Report.
6. UMLS-Encoded hypothetical Autopsy Report.
7. Health Insurance Portability and Accountability Act.
8. Privacy and Clinicopathologic Research.
9. Autopsy Example: Sickle Cell Disease.
10. Contingency Table Analysis.
12. Token Swap Test.
12. Token Swap Test: Null Hypothesis.
13. Token Swap Test: Internet Calculator.
14. The Problem: missing values; need; cost; what/what-not to collect.
15. Zermelo-Frankel Set Theory.
16. Zermelo-Frankel Set Theory Operations.
17. No Paradox of Self Reference.
18. Basic Concepts of the Theory.
19. Dicitur Homerum Caecum Esse.
20. Modal Logic/Complementizers.
21. St Peter's Rule.
22. Sutton's Law.
23. Basic Definitions.
24. Rule 1. Double-Negative=Positive. Complementizers absorb negatives.
25. Rule 2. Knowledge-Ordinal.
26. Rule 3. Data-absolute.
27. Rule 4. d-Hippocratic.
28. Rule 5. d-Conative.
29. Rule 6. keð..d-Vexative.
30. Rule 7. kðe-Ontologic.
31. Rule 8. Ethical-dative.
32. Rule 9. Covers.
33. Theorem 1a. Consistency before Data-collection.
34. Theorem 1a. Style of Proof.
35. Theorem 1b,c. Occam's Razor.
36. Computational Complexity. NP-complete. TSP.
37. Theorem 10.
38. Token Swap Method Revisited.
39. Loose Ends.
40. Summary. 1.
41. Summary. 2.
42. References.
43-52. Mathematical Appendix.
53. Prostate Cancer Example 1.
54. Prostate Cancer Example 2.
55. Prostate Cancer Example 3.

SCREEN 4. INTRODUCTION.

1. Data-mining in Anatomic Pathology: use of public data for drawing medical conclusions [1,2,3,4,5,6].
2. Constraints: patient privacy, missing values.
3. Data-mining program for pathology: incorporate constraints of routine medical practice.
4. Completing a rectangular database: may be unnecessary, uneconomic, technically unfeasible, or unethical.
5. Formal considerations for missing values, patient consent, patient risk, and provider alerts.
4. Set theory definitions of ATOMS, DATA, and MEDICAL ENTITIES [7,8,9,10]
5. Modal concepts of know-whether ($), need-to-know-whether (#), and try-to-know-whether (!) [11,12,13,14,15,16,17,18,19,20,21]

SCREEN 5. HYPOTHETICAL AUTOPSY REPORT

Male. Caucasian. 1.91 m. 95.5 kg. [22].
b. 8/27/1908. d. 1/22/1973.
Occupation: U.S. Congressman, U.S. Senator, U.S. President.
Status post: Appendectomy.
Status post: Cholecystectomy.
History of: Renal Calculi.
Myocardial Infarct, 1955.
Myocardial Infarct, April, 1972.
Myocardial Infarct, January 22, 1973.
Marked Generalized Atherosclerosis.

SCREEN 6. UMLS-ENCODED HYPOTHETICAL AUTOPSY REPORT [23,24,25]

Male. Caucasian. 1.91 m. 95.5 kg. {C0024554}.
b. 8/27/1908. d. 1/22/1973. {C0021132}.
Occupation: U.S. Congressman, U.S. Senator, U.S. President. {C0032382}.
Status post: Appendectomy. {C0003611}.
Status post: Cholecystectomy. {C0008320}.
History of: Renal Calculi. {C0022650}.
Myocardial Infarct, 1955. {C0027051}.
Myocardial Infarct, April, 1972. {C0027051}.
Myocardial Infarct, January 22, 1973. {C0027051}.
Marked Generalized Atherosclerosis. {C0205082,C0205046,C0205246}.

Privacy: Does the patient have a positive syphilis test?

Summary/Set theory definition: {{C0024554}, {C0021132}, {C0032382}, {C0003611}, {C0008320}, {C0022650}, {C0027051}, {C0027051}, {C0027051}, {C0205082,C0205046,C0205246}}.

SCREEN 7. HIPAA [26,27,28,29,30,31,32,33].

U. S. Health Insurance Portability and Accountability Act. 1996. (HIPAA, Kennedy-Kassebaum Bill, H.R. 3103 of 104th U. S. Congress).

2. Regulates all individually identifiable medical records in the USA.

3. Final Rule in force since April 14, 2003.

4. Huge fines for non-compliance: $25,000 apiece for each record disclosed unintentially, more for intentional disclosures or disclosures involving commercial gain.

5. Some research studies involving statistics require individual data.

6. For public research databases, no patient medical record may be individually identifiable.

7. The Johns Hopkins Autopsy Resource is temporarily shut down pending additional measures for HIPAA compliance.

SCREEN 8. PRIVACY AND CLINICOPATHOLOGIC RESEARCH [34].

1. Some research studies involving statistics require individual patient data.

2. Published, grouped data may not contain all the detail necessary to evaluate the statistical analysis methods.

3. Strong Privacy: The patient him/herself cannot identify his/her own medical record. Therefore, there must be c exact duplicates in the published record.

4. Weak Privacy: The public part of a patient's record cannot be uniquely identified. Therefore, there must be c exact duplicates in the public variables of the published record.

5. Dangers of Weak Privacy: embarrassment to the patient, even if logically unfounded; sense by the patient that his/her records are public, even if they are not; if one private part is disclosed, then the remainder of the record is exposed.

6. Detail must be blurred just enough so that one patient can be mistaken for another patient.

7. It is a bad idea, statistically, as well as fraudulent, to create additional, phantom patients.

SCREEN 9. PROTOTYPE AUTOPSY SERIES: SICKLE CELL CRISIS [35].

1. Pain crisis in sickle cell disease is a poorly localized abdominal pain that requires major pain medications. There are no characteristic morphologic features corresponding to pain crisis in sickle cell disease.

2. Can pain crisis in sickle cell disease be recognized statistically at autopsy?

3. Parfrey NA, Moore GW, Hutchins GM.
Is pain crisis a cause of death in sickle cell disease?
Am J Clin Pathol. 1985 Aug;84(2):209-212.

4. 71 autopsied cases of sickle cell disease in the autopsy files of The Johns Hopkins Medical Institutions with adequate clinical histories. 9/20 (45%) patients died in pain, death unexplained at autopsy; 4/51 (8%) patients died without pain, death unexplained at autopsy.

5. Is there a significant correlation between unexplained death and pain crisis?


__________Pain Crisis____ No Pain Crisis___
______________________________________
Unexplained |       |
___________________________________
Explained    |       |
___________________________________



SCREEN 10. CONTINGENCY TABLE ANALYSIS.

1. A 2 × 2 CONTINGENCY TABLE (2×2CT) is a rectangular table, two rows, two columns [35,36,37,38].

2. Rows represent an existing standard ("gold standard"); columns represent a new hypothesis.

3. Sampling assumptions are required by CHISQUARE TEST (CST) and FISHER EXACT TEST (FXT).

4. TOKEN SWAP TEST (TST): statistical-type significance test, that measures the likelihood of MISCLASSIFICATIONS in a (2×2CT)

5. The TST does not depend upon the usual statistical assumptions of repeated, random sampling from a source population.

SCREEN 11. TOKEN SWAP TEST.

1. TOKEN SWAP SIGNIFICANCE EXAMPLE. In the following example, it requires five TOKEN SWAPS to transform the expected into the observed contingency table:
  EXPECTED                EXPECTED+1                OBSERVED
 ---------------         ---------------           ---------------
 |  4 |  9 | 13          |  5 |  8 | 13            |  9 |  4 | 13 
 ---------------   -->   ---------------  -->-->   ---------------
 | 16 | 42 | 58          | 15 | 43 | 58            | 11 | 47 | 58
 ---------------         ---------------           ---------------
 | 20 | 51 | 71          | 20 | 51 | 71            | 20 | 51 | 71


2. The chances that these two swaps could have taken place AT RANDOM are:
         (9×16)
 = _________________________
   (9×16)+(4×42)
that is, the number of possible of EXPECTED-to-EXPECTED+1 swaps, divided by (the number of possible EXPECTED-to-EXPECTED+1 swaps plus the number of possible EXPECTED-to-EXPECTED-1 swaps), without altering the marginal totals.

3. When the EXPECTED has swapped up to the OBSERVED table, without altering the marginal totals, and the proportion of such swaps is less than 5%, then the result is significant.

SCREEN 12. TOKEN SWAP TEST NULL HYPOTHESIS.

1. The observed 2×2CT is NOT SO DIFFERENT from the expected 2×2CT that occasional misclassifications by a medical observer could account for the differences.



SCREEN 13. TOKEN SWAP TEST INTERNET CALCULATOR.

1. Enter cell totals in cell-boxes of contingency table.

2. Click on the SUBMIT button:

__________Pain Crisis____ No Pain Crisis___
______________________________________
Unexplained |       |
___________________________________
Explained    |       |
__________________________



SCREEN 14. THE PROBLEM: MISSING VALUES.

1. Cost(!). Every datum has a cost: inconvenience, needle-stick, financial payment,....

2. Need(#). Hippocrates [39]: only collect data that need to be collected.

3. What to collect, what not to collect: Vexation; Ontology.

SCREEN 15. ZERMELO-FRANKEL SET THEORY (ZFST).

1. Zermelo-Frankel Set Theory (ZFST) is ordinary set theory [7,8,9,10]

2. Undefined concepts of ZFST: is-a-member-of or belongs-to C; null-set or empty-set, Ø or {}.

3. Set is defined exactly by its members, arbitrary order.

4. Set-of-x not equal x; no repeat elements in a set.

5. Roster (extensional, list) notation: set O = {heart, lung, liver, pancreas, ...}.

6. Raster (intensional) notation: O = {x|x is a major-body-organ}.

SCREEN 16. ZERMELO-FRANKEL SET THEORY.

1. SUBSET: X c Y if and only if for every x C X, x C Y.

2. EQUALITY: X = Y if and only if X c Y and Y c X.

3. UNION: X U Y is the set of all x such that x C X or x C Y or both.

4. INTERSECTION: X /\ Y is the set of all x such that x C X and x C Y.

5. SUBTRACTION: X - Y is the set of all x such that x C X and x ~ C Y.

SCREEN 17. NO PARADOX OF SELF REFERENCE.

1. Epimenides the Cretan: All Cretans are liars.

2. St. Paul's Letter to Titus: 1:12. "One of themselves, even a prophet of their own, said, The Cretans are always liars, evil beasts, slow bellies...." [40].

3. Barber paradox: The barber shaves everyone who doesn't shave himself. Who shaves the barber?

4. Russell's Paradox (Letter to Frege): Set of all sets [41].

5. Berry Paradox: "The smallest positive integer not nameable in under eleven words." [42].

6. Baltimore VAMC patient states: All Baltimore VAMC patients are liars. Do you believe the medical history or not?

SCREEN 18. BASIC CONCEPTS OF THE THEORY.

1. Atomset, A, set of distinct, atomic statements (atoms, A), each with a definite true-false status.

2. Each atom is either a datum or a medical entity: (D U E) = A.

3. Data include complaints, history, physical findings, laboratory values, statements of consent, etc.

4. Medical entities include cancer, inflammation, necrosis, etc.

5. No datum is an entity and no entity is a datum: (D /\ E) = Ø.

6. To each atom, there exists known-to-the-k-a, $ka C $A, for every integer k up to a maximum, M.

7. To each datum, there exists need-to-know-d, #d C #D, and try-to-know-d, !d C !D.

SCREEN 19. DICITUR HOMERUM CAECUM ESSE.

1. DICITUR HOMERUM CAECUM ESSE. (Latin: It is said that Homer was blind.)

2. Modal part: DICITUR... It is said that...
Medical part: HOMERUM CAECUM ESSE.

3. Modal part: DICITUR SIVE... It is said whether...
Medical part: HOMERUM CAECUM ESSE (...SIVE HOMERUM NON CAECUM ESSE).

4. Modal part: COGNITUR SIVE... It is known whether...
Medical part: HOMERUM CAECUM ESSE....

5. Modal part: QUAERITUR SIVE... It is sought-to-know whether...
Medical part: HOMERUM CAECUM ESSE....

6. Modal part: CONATUR SIVE... It is tried-to-know whether...
Medical part: HOMERUM CAECUM ESSE....

7. It is known/needed-to-know/tried-to-know whether the patient's serum prostatic specific antigen is elevated.

8. It is known whether the patient has prostate cancer, +$prostatecancer.

SCREEN 20. MODAL LOGIC/COMPLEMENTIZERS.

1. Modal logic discusses the strength of a truth [4,5,6,7,11,12,13].

2. COGNITIVE ($): It is known whether...

3. QUISITIVE (#): It is needed-to-know whether...

4. CONATIVE (!): It is tried-to-know whether...

5. VENN DIAGRAM:

SCREEN 21. ST PETER'S RULE.

1. "...Thou art Peter, and upon this rock... and whatsoever thou shalt bind (ß) on earth shall be bound (ß) in heaven; and whatsoever thou shalt loose (£) on earth shall be loosed (£) in heaven...." [43].

2. ßa = a & $a.

3. £a = a | -$a.

4. ßa = -£-a; £a = -ß-a.

5. ßka = a & $ka.

6. £ka = a | -$ka.

SCREEN 22. SUTTON'S LAW.

1. Reporter: Willie, why to you always rob banks?
Willie Sutton: Because that's where the money is. [3,44].

2. Fever of Undermined Origin [45].

3. In the event of uncertainty, go where the money (i.e., the most likely result) is.

4. In the event of fever in a patient with cough, rusty sputum, shortness of breath, lobar pneumonia, go for streptococcal pneumonia, i.e., the most likely result, while waiting for culture results.

5. For data ð.. and entity e, ßkð..=> ßke|ßk+1-e,

SCREEN 23. BASIC DEFINITIONS.

1. CARDINALITY OF X, ñX, is number of elements in X.

2. M >1 is KNOWLEDGELADDER, $1a, $2a,..., $Ma.

3. Data are collected sequentially in steps 0, 1, 2,..., H, called DATABASELADDER, to comprise the KNOWLEDGE/DATABASE, denoted B0, B1, B2,..., BH.

4. G is the number of elements in the knowledge/database, BH, i.e., G = ñBH.

5. ATOMSET, A = {+a,-a,...}, where for every +a C A, -a C A, -a ~= a, ++a = +a, and --a = +a.
D = {+d,-d,...} is the set of DATA, where for every d C D, -d C D.
E = {+e,-e,...} is the set of ENTITIES, where for every e C E, -e C E.
(D U E) = A and (D /\ E) = Ø.

5. COMPLEMENTIZERS: $k, #, !, where for every 1 < k < M, and for every a C A, and d C D, a=$ka = $k-a, #d=#-d, and !d=!-d, where:
COGNITIVE, $ka: known-to-the-k whether a....
QUISITIVE, #d: need-to-know whether d....
CONATIVE, !d: try-to-know whether d....

6. FULLSET, F = {+f,-f,...}, where f C F if and only if: f C A; or for some a C A and 1 < k < M, f=$ka or f=-$ka, or for some d C D, f=#d, f=-#d, f=!d, or f=-!d.

7. WORLD, W, is the set of all w C W where w c F, i.e., W is the powerset of F, denoted ¶F.

8. The SET OF ALL POSSIBLE PATIENTS, or the POSSIBLE WORLDS, or the TRUTH TABLE, TcW [5], is the set of all t C T such that for every f C F, either f C t or -f C t, but not both.

9. NANDSET/NULLITY[3,4,46,47,48,49,50]: It is true that x1 | x2 | x3 |... for X if and only if {-x1,-x2,-x3,...} C X. NANDSETS have the property that if Y c Z, then Y implies Z.

10. For any X c W, the CONSEQUENCES OF X, ÇX, ÇX is the set of all y C ÇX such that for every t C T, y c t if and only if there exists an x C X such that x c t.

Claim: ÇX is computable after cG4 steps, for some constant, c.

SCREEN 24. RULE 1. DOUBLE-NEGATIVE=POSITIVE.
COMPLEMENTIZERS ABSORB NEGATIVES.

1. A = {+a,-a,...} is the ATOMSET.

2. For every +a C A, -a C A, -a ~= a, ++a = +a, and --a = +a.

3. For every +a C A, $ka = $ka.

SCREEN 25. RULE 2. KNOWLEDGE-ORDINAL.

1. ($ka=>$k-1a)@B0.

2. NANDSET DEFINITION: {+$ka,-$k-1a} C B0 for every k, 1 < k < M-1 and a C A.

3. VENN DIAGRAMS:
     

SCREEN 26. RULE 3. DATA-ABSOLUTE.

1. ($d=>$Md)@B0.

2. NANDSET DEFINITION: {$d,-$Md} C B0, for every d C D.

3. VENN DIAGRAMS:
     

SCREEN 27. RULE 4. d-HIPPOCRATIC.

1. (-#d=>-!d)@B0 [39].

2. NANDSET DEFINITION: {-#d,+!d} C B0, for d C D.

3. VENN DIAGRAMS:
     

SCREEN 28. RULE 5. d-CONATIVE.

1. ((-$d&#d)=>!d)@B0.

2. NANDSET DEFINITION: {-$d,+#d,-!d} C B0, for d C D.

3. VENN DIAGRAMS:
     

SCREEN 29. RULE 6. keð..d-VEXATIVE.

1. (ßke&ßkð, ...,&-$d)=>(#d| ßk+1-e) @ B0.

2. NANDSET DEFINITION: {+$ke,e,+$kð,ð,..,-$d,-#d, -$k+1e} C B0, for 1 < k < M-2, ðC D, and e C E.

3. The keð..d-vexative definition supports a VOBIS-DIFFICILE CONDITION (Latin: Difficult-thing for you).

4. A condition that is easy for some patients but difficult for others.

SCREEN 30. RULE 7. kð...e-ONTOLOGIC.

1. Ontology: Platonic description of essential reality [51,52,53,54,55].

2. Contrast: what one can see (observation, accident); what one can know (epistemology); what one can believe (doxology); other aspects of perceiving reality.

3. Metaphysical commitments or presuppositions embodied in natural sciences.

4. Example: belief that a cancer can metastasize.

5. In medical informatics, ontology is a structured list of concepts and relations among concepts.

6. Typically prepared by an expert or panel of experts.

7. (ßkð..)=> (ßke|ßk+1-e) @ B0, 1<k<M-2.
What is ßM-e?

"Alle Kunst
Ist umsunst
Wenn der Engel
Auf dem Zundloch brunst."

All artifice is in vain when the angel urinates on your musket.

Quoted by Rudolf Breitnaecker, MD, in his lecture on forensic pathology to Johns Hopkins Medical School second-year pathology students, February, 1977.


8. VENN DIAGRAMS:
           

9. NANDSET DEFINITION: {+$kð,ð,..,-e,-$k+1e} C B0, for 1 < k < M-2, d C D, ð c (D - {+d,-d}).

SCREEN 31. RULE 8. ETHICAL-DATIVE.

0. If d is d-Hippocratic, then there exists at most one I, 1 < I < H, such that:
1. (POS-DATA): +$d, +d, +!d true for BI, xor
2. (NEG-DATA): +$d, -d, +!d true for BI, xor
3. (FAIL-DATA): -$d, +!d true for BI, xor
4. (NOTRY-DATA): -$d, +$d, -#d, +#d, -!d, +!d not true for BI.

SCREEN 32. RULE 9. COVER.

1. It is true that -$ka @ CI if and only if it is not true that $ka @ ÇBI

2. NANDSET DEFINITION: {$ka} C CI if and only if {-$ka} ~ C ÇBI, for 1 < I < H, 1 < k < M, and a C A.

SCREEN 33. THEOREM 1a. THEOREM 1. CONSISTENCY OF B0

1. B0 IS CONSISTENT.

2. NANDSET DEFINITION: Ø ~C ÇB0.

SCREEN 34. THEOREM 1a. STYLE OF PROOF.

To demonstrate that Ø ~C ÇB0, it suffices to construct a possible-patient / truth-table-element, t' that is NOT A SUPERSET of any member of B0. For if every t were a superset of some member of B0, since every t is a superset of Ø, it would follow that Ø C ÇB0, so that B0 would be inconsistent.

For this demonstration, construct t' such that every modal member of t' is negative. That is: t' = {-$kd, -$k-1d, -$d, -#d, -!d, ... -$ke, -$k-1e...}, for every k, d, e. (The (non-modal) values of d, e do not matter.) Then:

| B0 element: | Set Definition: | Possible Patient
| Rule 2. KwnlOrd$kd | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KnwlOrd$ke | {-$ke,+$k+1e} | ...-$k+1e... | 1<k<M-1
| Rule 3. DataAbs$d | {+$d,-$Md} | ... -$d ... |
| Rule 4. d-Hippocr | {-#d,+!d} | ... -!d ... |
| Rule 5. d-Conative | {-$d,+#d,-!d} | ... -#d ... |
| Rule 6. keð..d-Vex | {+$ke,e,+$kð,+ð,-$d,-#d,-$k+1e} | ...-$ke... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-e,-$k+1e} | ...-$kð... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð, -$ke} | ...-$kð... | 1<k<M-2.

SCREEN 35. THEOREM 1b,c,d. OCCAM'S RAZOR.


Theorem. 1b. No $d is true for ÇB0. Occam's Razor: No data are implied without data.
Theorem. 1c. No $e is true for ÇB0 Occam's Razor: No entities are implied without data.
Theorem. 1d. No #d is true for ÇB0 Occam's Razor: No data are needed without other data.

SCREEN 36. COMPUTATIONAL COMPLEXITY.

1. Computational complexity is the quantity of computer resources necessary to complete a particular computer algorithm, involving G data elements [56,57,58].

2. An algorithm is LINEAR COMPLETE if one can successfully complete the algorithm after c×G steps, for constant c. Example: finding and fetching a single element in an unsorted list.

3. An algorithm is LOG COMPLETE if one can successfully complete the algorithm after c×logbG steps, where typically b=2, i.e., complete after c×log2G steps. Example: finding and fetching a single element in a sorted list, using the heapsort or quicksort method.

4. An algorithm is LOG-LINEAR COMPLETE if one can successfully complete the algorithm after c×nlog2G steps. Example: creating a sorted list, using the heapsort or quicksort method.

5. An algorithm is said to be QUADRATIC COMPLETE if one can successfully complete the algorithm after c×G2 steps;

6. An algorithm is CUBIC COMPLETE if one can successfully complete the algorithm after c×G3 steps;

7. An algorithm is QUARTIC COMPLETE if one can successfully complete the algorithm after c×G4 steps;

8. In general, an algorithm is POLYNOMIAL COMPLETE if one can successfully complete the algorithm after c×G4 steps, for some integer constant, k.

9. An algorithm is EXPONENTIAL COMPLETE, if one can successfully complete the algorithm after c&×2G steps. An exponential-complete algorithm is essentially hopeless for most practical computing problems.

10. An algorithm is FORMALLY INCOMPLETE if one cannot successfully complete the algorithm after any number of steps, so-called Gödel-undecidability [56,59,60,61].

11. A very famous class of computer algorithms is NON-POLYNOMIAL COMPLETE (NP-COMPLETE), i.e., at worst exponential complete, but for which it is unknown whether a polynomial complete algorithm exists.

12. In this report, we claim that the algorithm for solving the consequences of BH is quartic-complete, i.e, soluble after cG4 steps, where G = ñBH

13. TRICK: G could be very large, say, possibly up to 2(ñA). The assumption is that physician ontologies are not that intricate.

SCREEN 37. THEOREM 10.

The number of calculations to obtain ÇBH is equal to c×G4, for some constant c.

SCREEN 38. TOKEN SWAP METHOD REVISITED.

The TOKEN SWAP TEST (TST) is a statistical test for analyzing data in a 2×2 CONTINGENCY TABLE (2×2CT). The 2×2CT is the backbone of hypothesis-testing in clinicopathologic (case series) research. For example, if there is an entity, e, predicted by data, ð..., then a clinicopathologic patient series might yield the results:
                           ße
                        -    +
                  ------------------
                  -  |  a |  b |  v 
      ßð          ------------------
                  +  |  c |  d |  w 
                  ------------------
                     |  x |  y |  z 
where ß-ð are the patients for which data are negative;
ß+ð are the patients for which data are positive;
ß-e are the patients for which the entity is negative; and
ß+e are the patients for which the entity is positive.
Values a, b, c, d comprise the CELL TOTALS, where a is the number of patients with
ß-ð & ß-e, i. e., necessarily not-ð and necessarily not-e;
b is the number of patients with
ß-ð & ß+e, i. e., necessarily not-ð and necessarily e;
c is the number of patients with ß+ð & ß-e, i. e., necessarily not-ð and necessarily not-e;
and d is the number of patients with ß+ð & ß+e, i. e., necessarily not-ð and necessarily e;
Values v, w, x, y comprise MARGINAL TOTALS, where v = a + b; w = c + d; x = a + c; y = b + d.
Value z is the GRAND TOTAL, where z = v + w = x + y = a + b + c + d.

The token swap test examines the assertion that ß+ð=>ß+e and ß-ð=>ß-e, or more precisely, ßk+ð=>(ßk+e|ßk+1-e) and ßk-ð=>(ßk-e|ßk+1+e).

SCREEN 39. LOOSE ENDS.

1. Computer Translation [62,63,64,65,66,67,68,69,70]: How does Marked Generalized Atherosclerosis get translated into: {C0205082,C0205046,C0205246}.

2. Zipf's Law for Word Distributions [71,72,73,74]: f = (k/r), where f is the frequency of a particular word; and r is the rank of that word in the descending-order word distribution (of=rank-1, and=rank-2, the=rank-3, etc.).

3. Zipf's Law Part A: Common words are very common.
Zipf's Law Part B: Uncommon words are composites of uncommon words.

4. Zipf's Law for Phrase Distributions.

5. Zipf's Law for Grammar Distributions.

SCREEN 40. SUMMARY.

1. Pathology studies the etiology and pathogenesis of disease.

2. Any data-mining program must incorporate the fundamental constraints on data acquisition in routine medical practice.

3. Some data are unnecessary, uneconomic, technically unfeasible, or unethical to collect.

4. Mathematically consistent theory of clinicopathologic inference.

5. Modal concepts of know-whether ($), need-to-know-whether (#), and try-to-know-whether (!).

6. Occam's Razor: no entities are known without data.

7. d-Hippocratic, d-conative, keð..d-vexative, and kðe-ontologic properties: consistent if data are entered consensually, consecutively, and consistently.

8. Computer algorithm concludes within polynomial time.

SCREEN 40. SUMMARY.



9. Theory is completely general.

10. Definitions of patient injury include possible death, morbidity, inconvenience, financial constraints, or loss-of-privacy.

11. Definitions of need-to-know may differ among observers: patient, physician, insurer, national health policy, research protocol.

12. There are, for example, numerous patients in computerized systems (the 172 Veterans Affairs hospitals, serving 2,500,000 patients, for example) which could employ a systematic mechanism for alerting providers to necessary upcoming events, such as an annual hemoglobin a1c and podiatry examination for diabetic patients.

13. Such a computer mechanism amounts to moving points from the clear space in the Screen #27 Venn Diagram into the blue area (i.e., developing a concept space); and from the blue area into the central gray area (i.e., seeing the patients).

14. Mathematical theories can organize medical knowledge, and improve the scheduling and effectiveness of data collection and surveillance.

SCREEN 41. REFERENCES.

1. Moore GW, Berman JJ.
Anatomic Pathology Data Mining. Chapter 4.
In: Cios KJ. Medical Data Mining and Knowledge Discovery. Published, December 4, 2000, within the series: "Studies in Fuzziness and Soft Computing", Physica-Verlag Heidelberg, a Springer-Verlag Company. Cios, K.J., University of Colorado at Denver, CO, USA. (Ed.).
Medical Data Mining and Knowledge Discovery.
2001. XVIII, 502 pp. 98 figs., 98 tabs. Hardcover.
ISBN: 3-7908-1340-0, 502 pages.

2. Moore GW, Boitnott JK, Miller RE, Eggleston JC, Hutchins, GM.
Integrated anatomic pathology reporting system using natural language diagnoses.
Modern Pathol. 1988;1:44-50.

3. Moore GW, Hutchins GM.
Symbolic logic analysis of congenital heart disease.
Pathol Res Pract. 1981 Mar;171(1):59-85.

4. Moore GW, Hutchins GM, Bulkley BH.
Certainty levels in the nullity method of symbolic logic: application to the pathogenesis of congenital heart malformations.
J Theor Biol. 1979 Jan 7;76(1):53-81.

5. Moore GW, Hutchins GM.
A Hintikka possible worlds model for certainty levels in medical decision making.
Synthese. 48:87-119, 1981.

6. Moore GW, Hutchins GM.
Consistency versus completeness in medical decision-making: Exemplar of 155 patients autopsied after coronary artery bypass graft surgery.
Med Inform (Lond). 1983 Jul-Sep;8(3):197-207.

7. Lewis CI, Langford CH. Symbolic Logic. Second Edition.
New York: Dover Publications, Inc. 1932;:.
ISBN 0-486-60170-6, 518 pages.

8. Suppes P.
Axiomatic Set Theory.
Princeton, NJ: D. Van Nostrand Company, Inc. 1960;:. The University Series in Mathematics.
ISBN not stated, 265 pages.

9. Halmos PR.
Naive Set Theory.
Princeton, NJ: D. Van Nostrand Company, Inc. 1960;:. The University Series in Mathematics.
ISBN not stated, 104 pages.

10. Moore GW, Goodman M.
A set theoretical approach to immunotaxonomy: Analysis of species comparisons in modified Ouchterlony plates.
Bull Math Biophys. 1968 Jun;30(2):279-289.

11. Zadeh LA.
From computing with numbers to computing with words. From manipulation of measurements to manipulation of perceptions.
Ann N Y Acad Sci. 2001 Apr;929:221-252. Review.
PMID: 11357866

12. Sadegh-Zadeh K.
Advances in fuzzy theory.
Artif Intell Med. 1999 Mar;15(3):309-323.
PMID: 10206113

13. Zadeh LA.
A note on prototype theory and fuzzy sets.
Cognition. 1982 Nov;12(3):291-297.
PMID: 6891312

14. Dorsey DW, Coovert MD.
Mathematical modeling of decision making: a soft and fuzzy approach to capturing hard decisions.
Hum Factors. 2003 Spring;45(1):117-135.
PMID: 12916585

15. Moore GW, Hutchins GM.
Effort and demand logic in medical decision making.
Metamedicine. 1980;1:277-304.

16. Zeman J.
Modal Logic, The Lewis-Modal Systems.
Oxford: Oxford University Press. 1973;:.
ISBN not stated, 302 pages.

17. Lukasiewicz J.
Elementy Logiki Matematycznej.
Warsaw. 1929;:.
as cited in Zeman, 1973.

18. Lukasiewicz J.
A system of Modal Logic.
The Journal of Computing Systems. 1953;1:111-149.
as cited in Zeman, 1973.

19. Lukasiewicz J.
Arithmetic and Modal Logic.
The Journal of Computing Systems. 1953;1:213-219.
as cited in Zeman, 1973.

20. Lukasiewicz J.
On a Controversial Problem of Aristotle's Modal Syllogistic.
Dominican Studies. 1954;7:114-123.
as cited in Zeman, 1973.

21. Garson J.
Modal Logic.
The Stanford Encyclopedia of Philosophy (Winter 2001 Edition)
Edward N. Zalta, ed.
http://plato.stanford.edu/archives/win2001/entries/logic-modal/

22. Degregorio WA.
The Complete Book of U.S. Presidents. Fifth Edition.
New York: Barricade Books. 1997;:.

23. U. S. National Library of Medicine, Unified Medical Language System.
http://www.nlm.nih.gov/research/umls/

24. Sinard JH, Moore GW.
UMLS Concordance for a Comprehensive Pathology Text.
Arch Pathol Lab Med. 2001;:in press.
http://www.netautopsy.org/apep01op.htm

25. Moore GW, Brenner DS, Berman JJ.
Automatic Indexing of a Pathology Image Archive using UMLS.
Arch Pathol Lab Med. 2000;124:809.
http://www.netautopsy.org/apep99im.htm

26. U. S. Code of Federal Regulations. 1995. 45 CFR Subtitle A (10-1-95 Edition), part 46.101 (b) (4). U. S. Department of Health and Human Services. Office of the Secretary.
The complete Common Rule document (45CFR46), at URL:
http://www.uaf.edu/oar/irb/45cfr46.html
or at URL:
http://ohrp.osophs.dhhs.gov/humansubjects/guidance/45cfr46.htm

27. The University of Mississippi has published its Multiple Project Assurance Document at URL:
http://www.olemiss.edu/depts/research/irb/assurance.htm

28. National Cancer Institute's Confidentiality Brochure, at URL:
http://www-cdp.ims.nci.nih.gov/policy.html

29. U. S. Code of Federal Regulations. 1999. 45 CFR Parts 160 - 164. Standards for Privacy of Individually Identifiable Health Information; Proposed Rule. Department of Health and Human Services. Office of the Secretary.
Fed Regist. 1999 Nov 3;64(212):59917-59966. http://aspe.hhs.gov/admnsimp/

30. U. S. Health Insurance Portability and Accountability Act. 1996. (HIPAA, Kennedy-Kassebaum Bill, H.R. 3103 of 104th U. S. Congress). U. S. Government Documents at URL:
http://thomas.loc.gov

31. U. S. National Bioethics Advisory Commission (NBAC). 1995.
http://bioethics.gov/general.html
Executive Order 12975, October 3, 1995.
Federal Register: October 5, 1995. v. 60.; no. 193. pp. 52063-52065

32. National Bioethics Advisory Commission (NBAC), Recommendations to the Common Rule:
http://bioethics.gov/pubs.html

33. Office of Human Research Protections (OHRP), within OPHS, DHHS (formerly, Office for Protection from Research Risks (OPRR)), at URL:
http://ohrp.osophs.dhhs.gov

34. Moore GW, Brown LA, Miller RE.
Set Theory Definition and Algorithm for Medical De-Identification.
Arch Pathol Lab Med. 2001;:in press.
http://www.netautopsy.org/apep00st.htm

35. Parfrey NA, Moore GW, Hutchins GM.
Is pain crisis a cause of death in sickle cell disease?
Am J Clin Pathol. 1985 Aug;84(2):209-212.
PMID: 4025226.
PubMed Entry

36. Moore GW, Hutchins GM, Miller RE.
Token swap test of significance for serial medical data bases.
Am J Med. 1986 Feb;80(2):182-190.
PMID: 3511687.
PubMed Entry

37. Moore GW, Hutchins GM, Miller RE.
A new paradigm for hypothesis testing in medicine, with examination of the Neyman Pearson condition.
Theor Med. 1986 Oct;7(3):269-282.
PMID: 3798393.
PubMed Entry

38. Heckering PS.
Token swap test revisited.
Comput Methods Programs Biomed. 2003 Mar;70(3):265-269.
PMID: 12581559.
PubMed Entry

39. Hippocrates.
Hippocrates. Volume I.
Jones WHS, transl. Loeb Classical Library. Cambridge, MA: Harvard University Press. 1923.
ISBN 0-674-99162-1, 361 pages.
Includes Hippocrates' Oath, with explanatory notes.
According to:
http://www.geocities.com/everwild7/noharm.html
"First, Do No Harm" Is Not in the Hippocratic Oath, but rather in Epidemics, Bk. 1, Sect. 11. One translation reads: 'Declare the past, diagnose the present, foretell the future; practice these acts. As to diseases, make a habit of two things: to help, or at least to do no harm.'
This note supplied by Harris G. Yfantis, MD.

40. Titus 1:12. The Holy Bible. King James Version.

41. Irvine AD.
Russell's Paradox.
The Stanford Encyclopedia of Philosophy (Summer 2003 Edition).
http://plato.stanford.edu/archives/sum2003/entries/russell-paradox/

42. Berry paradox.
From Wikipedia, the free encyclopedia.
http://www.wikipedia.org/wiki/Berry_paradox

43. Matthew 16:18-19. The Holy Bible. King James Version.
"Keys to the Kingdom" may be regarded as a mathematical function, that is one-to-one and onto.

44. Sutton W, Linn E.
Where the Money Was. The Memoirs of the World's Greatest Bank Robber.
New York: Ballantine Books. 1976;:.
ISBN 0-345-25371-X-195, 422 pages.
Part Two: Breaking Out. Sutton's Law, pp. 148-150.

45. Petersdorf RG, Beeson PB.
Fever of Unexplained Origin.
Medicine. 1961;40:1-30.
Remark about Sutton's Law on p. 27.

46. Quine WV.
Theory of Deduction.
Cambridge, MA: Harvard Cooperative Society. 1948;:65-81.

47. Quine WV.
Methods of Logic.
New York: Henry Holt & Co. 1950;:.

48. Quine WV.
The problem of simplifying truth functions.
Am Math Monthly. 1952;59:521-531.

49. Quine WV.
A way to simplify truth functions.
Am Math Monthly. 1955;62:627-631.

50. McCluskey EJ jr.
Minimization of Boolean Functions.
Bell Syst Tech J 1956;36:1417-1444.

51. Smith B.
Mereotopology: A Theory of Parts and Boundaries.
Data and Knowledge Engineering. 1996;20:287-303.

52. Quine WVO.
Ontological relative, and other essays.
New York: Columbia University Press. 1969;:.

53. U. S. Defense Advanced Research Projects Agency (DARPA). Agent Markup Language.
http://www.daml.org

54. U. S. Defense Advanced Research Projects Agency (DARPA). Ontology Inference Layer.
http://www.ontoknowledge.org/oil

55. Breitnaeker R. 1977;:.

"Alle Kunst
Ist umsunst
Wenn der Engel
Auf dem Zundloch brunst."

All artifice is in vain when the angel urinates on your musket.

Quoted by Rudolf Breitnaeker, MD, in his lecture on forensic pathology to Johns Hopkins Medical School second-year pathology students, February, 1977.


56. Tarjan RE.
Data Structures and Network Algorithms. CBMS-NSF Regional Conference Series in Applied Mathematics.
Paperback, December, 1983.
New York: Society for Industrial & Applied Mathematics.
ISBN: 0898711878.

57. Davis M.
What is a computation?.
In: Steen LA, Mathematics Today. Twelve Informal Essays.
New York: Springer-Verlag. 1978;:.
ISBN 0-387-90305-4, 367 pages.

58. Stewart I.
Concepts of Modern Mathematics.
New York: Dover Publications, Inc. 1975;:.
ISBN 0-486-28424-7, 339 pages.
Discusses the NP complete computability problem.

59. Gödel K.
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. I.
Monatsh. Math. Phys. 1931;38:173-198.

60. Nagel E, Newman JR.
Gödel's Proof.
New York: New York University Press. 1958;:.
ISBN 0-8147-0325-9, 118 pages.

61. Casti JL, DePauli W.
Gödel. A Life of Logic. Cambridge, MA: Perseus Publishing. 2000;:.
ISBN 0-7382-0274-6, 210 pages.

62 Newmeyer FJ.
Generative Linguistics. A historical Perspective.
London: Routledge. 1996.

63. Chomsky N.
Aspects of the Theory of Syntax.
Cambridge, MA: The MIT Press. 1965;:.

64. Chomsky N.
Language and Mind.
San Diego: Harcourt Brace Jovanovich. 1968;:.

65. Hutchins WJ.
Machine Translation : Past, Present, Future .
Ellis Horwood/Wiley, Chichester/New York. 1986;:. Ellis Horwood Series in Computers and Their Applications. ASIN: 0135435218 .

66. Nagao M. Machine Translation.
In: Shapiro SC, ed. Encyclopedia of Artificial Intelligence. Volume 2. M-Z.
New York: Wiley-Interscience. 1992;:898-902.

67. Moore GW, Miller RE, Hutchins GM.
Microcomputer translator for medical text: Theorem verification for Chapter Two of Zeman's Modal Logic.
Adv Math Comput Med. 7:1621-1633, 1986.

68. Moore GW, Riede UN, Polacsek RA, Miller RE, Hutchins GM.
Automated translation of German to English medical text.
Am J Med. 1986 Jul;81(1):103-111.
PMID: 3755289; UI: 86265731.

69. Moore GW, Hutchins GM, Miller RE.
Examination of disease names using non-Abelian symbolic logic.
Methods Inf Med. 1986 Apr;25(2):109-115.
PMID: 3702747; UI: 86202865.

70. Moore GW, Wakai I, Satomura Y, Giere W.
TRANSOFT: Medical translation expert system.
Artif Intell Med 1:149-157, 1989.

71. Zipf GK.
Human Behavior and The Principle of Least Effort. An Introduction to Human Ecology.
Reading, MA: Addison-Wesley Press. 1949;:19-55.

72. Giere W.
Foundations of clinical data automation in cooperative programs.
Proc 5th Ann Symp Comp Applic Med Care. 1981;5:1142-1148.

73. Fedorowicz J.
A Zipfian model of an automatic bibliographic system: An application to MEDLINE.
J Am Soc Info Sci 1982;33:223-232.

74. Condon EU.
Statistics of vocabulary.
Science 1928;67:300, 1928.

SCREEN 43. THEOREM 1. CONSISTENCY OF B0

 

Theorem 1a. B0 is consistent: Ø ~CÇB0.
Theorem 1b. No $d is true for ÇB0. Occam's Razor: No data are implied without data: {-$d} ~CÇB0.
Theorem 1c. No $e is true for ÇB0 Occam's Razor: No entities are implied without data: {-$e} ~CÇB0.
Theorem 1d. No #d is true for ÇB0 Occam's Razor: No data are needed without other data: {-#d} ~CÇB0.
Proof: To demonstrate that Ø ~C ÇB0, it suffices to construct any possible-patient / truth-table-element, t' that is NOT A SUPERSET of any member of B0. For if every t were a superset of some member of B0, since every t is a superset of Ø, it would follow that Ø C ÇB0, so that B0 would be inconsistent.

For this demonstration, construct t' such that every modal member of t' is negative. That is: t' = {-$kd, -$k-1d, -$d, -#d, -!d, ... -$ke, -$k-1e...}, for every k, d, e. t' belongs to the outside (uncolored) space in the Venn diagram, above. The (non-modal) values of d, e do not matter in the proof. Then:

| B0 element: | Set Definition: | Possible Patient
| Rule 2. KwnlOrd$kd | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KnwlOrd$ke | {-$ke,+$k+1e} | ...-$k+1e... | 1<k<M-1
| Rule 3. DataAbs$d | {+$d,-$Md} | ... -$d ... |
| Rule 4. d-Hippocr | {-#d,+!d} | ... -!d ... |
| Rule 5. d-Conative | {-$d,+#d,-!d} | ... -#d ... |
| Rule 6. keð..d-Vex | {+$ke,e,+$kð,+ð,-$d,-#d,-$k+1e} | ...-$ke... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-e,-$k+1e} | ...-$kð... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-$ke} | ...-$kð... | 1<k<M-2.

Part (a). Thus, Ø ~CÇB0, because Ø c t'.
Part (b). By Definition of C0, {-$d} ~CÇB0, because {-$d} c t'. Thus, {$d} C C0, by Definition of Cover.
Part (c). By Definition of C0, {-$e} ~CÇB0, because {-$e} c t'. Thus, {$e} C C0, by Definition of Cover.
Part (d). By Definition of C0, {-#d} ~CÇB0, because {-#d} c t'.

SCREEN 44. THEOREM 2.

 
THEOREM 2. Ø ~CÇBH
Proof: Construct t' as follows. For each e, {-$Me,+$M-1e,...,±e} c t'. For each d, if d is:
notry, then let {-$Md,-$M-1d,...,-#d,-!d,±d} c t';
failed, then let {-$Md,-$M-1d,...,+#d,+!d,±d} c t';
positive, then let {+$Md,+$M-1d,...,+#d,+!d,+d} c t';
negative, then let {+$Md,+$M-1d,...,+#d,+!d,-d} c t'.
Then t'~C BH, as follows:

| B0 element: | Set Definition: | Possible Patient
| Rule 2. KwnlOrd$kd/notry | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/fail | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/pos | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KwnlOrd$kd/neg | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KnwlOrd$Me | {-$M-1e,+$Me} | ...-$Me... |
| Rule 2. KnwlOrd$ke | {-$ke,+$k+1e} | ...+$k+1e... | 1<k<M-1
| Rule 3. DataAbs$d/notry | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/fail | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/pos | {+$d,-$Md} | ... +$Md ... |
| Rule 3. DataAbs$d/neg | {+$d,-$Md} | ... +$Md ... |
| Rule 4. d-Hippocr/notry | {-#d,+!d} | ... -!d ... |
| Rule 4. d-Hippocr/fail | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/pos | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/neg | {-#d,+!d} | ... +#d ... |
| Rule 5. d-Conativ/notry | {-$d,+#d,-!d} | ... -#d ... |
| Rule 5. d-Conativ/fail | {-$d,+#d,-!d} | ... +!d ... |
| Rule 5. d-Conativ/pos | {-$d,+#d,-!d} | ... +$d ... |
| Rule 5. d-Conativ/neg | {-$d,+#d,-!d} | ... +$d ... |
| Rule 6. keð..d-Vex | {+$ke,e,+$kð,+ð,-$d,-#d,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-e,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-$ke} | ...+$ke... | 1<k<M-2.
| BH element: | Set Definition: | Possible Patient
| Rule 8. pos | {-$Md},{-d},{-!d} | ...+$Md ...+!d,...+d... |
| Rule 8. neg | {-$Md},{+d},{-!d} | ...+$Md ...+!d,...-d... |
| Rule 8. fail | {$d},{-!d} | ...-$d,...+!d,... |

SCREEN 45. THEOREM 3.

 
THEOREM 3. For every k, 1< k<M, and for every d C D:
{$d} C CI if and only if {d} ~C BI or {-d} ~C BI.
Proof: If. If {d} C BI or {d} C BI, then By SUBSET COROLLARY.
Only If. Construct t' as follows. For each e, {-$Me,+$M-1e,...,±e} c t'. For each d, if d is:
notry, then let {-$Md,-$M-1d,...,-#d,-!d,±d} c t';
failed, then let {-$Md,-$M-1d,...,+#d,+!d,±d} c t';
positive, then let {+$Md,+$M-1d,...,+#d,+!d,+d} c t';
negative, then let {+$Md,+$M-1d,...,+#d,+!d,-d} c t'.
Then t'~C BH, as follows: Then t' ~C BI, as follows:

| B0 element: | Set Definition: | Possible Patient
| Rule 2. KwnlOrd$kd/notry | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/fail | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/pos | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KwnlOrd$kd/neg | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KnwlOrd$Me | {-$M-1e,+$Me} | ...-$Me... |
| Rule 2. KnwlOrd$ke | {-$ke,+$k+1e} | ...+$k+1e... | 1<k<M-1
| Rule 3. DataAbs$d/notry | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/fail | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/pos | {+$d,-$Md} | ... +$Md ... |
| Rule 3. DataAbs$d/neg | {+$d,-$Md} | ... +$Md ... |
| Rule 4. d-Hippocr/notry | {-#d,+!d} | ... -!d ... |
| Rule 4. d-Hippocr/fail | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/pos | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/neg | {-#d,+!d} | ... +#d ... |
| Rule 5. d-Conativ/notry | {-$d,+#d,-!d} | ... -#d ... |
| Rule 5. d-Conativ/fail | {-$d,+#d,-!d} | ... +!d ... |
| Rule 5. d-Conativ/pos | {-$d,+#d,-!d} | ... +$d ... |
| Rule 5. d-Conativ/neg | {-$d,+#d,-!d} | ... +$d ... |
| Rule 6. keð..d-Vex | {+$ke,e,+$kð,+ð,-$d,-#d,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-e,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-$ke} | ...+$ke... | 1<k<M-2.
| BI element: | Set Definition: | Possible Patient
| Rule 8. pos | {-$Md},{-d},{-!d} | ...+$Md ...+!d,...+d... |
| Rule 8. neg | {-$Md},{+d},{-!d} | ...+$Md ...+!d,...-d... |
| Rule 8. fail | {$d},{-!d} | ...-$d,...+!d,... |

Proof(b): By Data-absolute.

SCREEN 46. THEOREM 4.

THEOREM 4. For every k, 1< k<M, and for every e C E:
if {-$e} &126;C ÇBICI, then {+e} ~C ÇBICI and {-e} ~C ÇBICI.
Proof. Let {-$e} &126;C ÇBICI, and without loss of generality, suppose that {-e} C ÇBICI. By Definition of Cover, {$e} C CI. Construct truth-table-element, t', such that {-e, -$e, -$2e} c t', where it must be true that t' C ÇBICI. The only way that this could be true is if Rule 7 contains {-e, -$e, -$2e}, whence it must be true that Rule 7 contains {-e, +$e, -$2e};
{-e, -$e, -$2e}; and
{-e, -$e, +$2e}..... Then ÇBICI. contains {-$e}. Contradiction. It is notable that the converse of the theorem is not necessarily true.

SCREEN 47. THEOREM 5.

 
THEOREM 5. CONSISTENCY OF BICI. Ø ~C ÇCIBI
Proof: If. By Subset Corollary.
Only if: Then t' ~C BH, as follows:

| B0 element: | Set Definition: | Possible Patient
| Rule 2. KwnlOrd$kd/notry | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/fail | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/pos | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KwnlOrd$kd/neg | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KnwlOrd$Me | {-$M-1e,+$Me} | ...-$Me... |
| Rule 2. KnwlOrd$ke | {-$ke,+$k+1e} | ...+$k+1e... | 1<k<M-1
| Rule 3. DataAbs$d/notry | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/fail | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/pos | {+$d,-$Md} | ... +$Md ... |
| Rule 3. DataAbs$d/neg | {+$d,-$Md} | ... +$Md ... |
| Rule 4. d-Hippocr/notry | {-#d,+!d} | ... -!d ... |
| Rule 4. d-Hippocr/fail | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/pos | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/neg | {-#d,+!d} | ... +#d ... |
| Rule 5. d-Conativ/notry | {-$d,+#d,-!d} | ... -#d ... |
| Rule 5. d-Conativ/fail | {-$d,+#d,-!d} | ... +!d ... |
| Rule 5. d-Conativ/pos | {-$d,+#d,-!d} | ... +$d ... |
| Rule 5. d-Conativ/neg | {-$d,+#d,-!d} | ... +$d ... |
| Rule 6. keð..d-Vex | {+$ke,e,+$kð,+ð,-$d,-#d,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-e,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-$ke} | ...+$ke... | 1<k<M-2.
| BI element: | Set Definition: | Possible Patient
| Rule 8. pos | {-$Md},{-d},{-!d} | ...+$Md ...+!d,...+d... |
| Rule 8. neg | {-$Md},{+d},{-!d} | ...+$Md ...+!d,...-d... |
| Rule 8. fail | {$d},{-!d} | ...-$d,...+!d,... |

SCREEN 48. THEOREM 6.

 
THEOREM 6. ÇBICI is d-Hippocratic if and only if B0 is d-Hippocratic.
Proof: If. If B0 is d-Hippocratic, then by Definition 24 (Rule 4), {-#d,+!d} C B0. By SUBSET COROLLARY, {-#d,+!d} C B0 c BI c ÇBICI. QED.
Only if: Then t' ~C BH, as follows:

| B0 element: | Set Definition: | Possible Patient
| Rule 2. KwnlOrd$kd/notry | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/fail | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/pos | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KwnlOrd$kd/neg | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KnwlOrd$Me | {-$M-1e,+$Me} | ...-$Me... |
| Rule 2. KnwlOrd$ke | {-$ke,+$k+1e} | ...+$k+1e... | 1<k<M-1
| Rule 3. DataAbs$d/notry | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/fail | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/pos | {+$d,-$Md} | ... +$Md ... |
| Rule 3. DataAbs$d/neg | {+$d,-$Md} | ... +$Md ... |
| Rule 4. d-Hippocr/notry | {-#d,+!d} | ... -!d ... |
| Rule 4. d-Hippocr/fail | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/pos | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/neg | {-#d,+!d} | ... +#d ... |
| Rule 5. d-Conativ/notry | {-$d,+#d,-!d} | ... -#d ... |
| Rule 5. d-Conativ/fail | {-$d,+#d,-!d} | ... +!d ... |
| Rule 5. d-Conativ/pos | {-$d,+#d,-!d} | ... +$d ... |
| Rule 5. d-Conativ/neg | {-$d,+#d,-!d} | ... +$d ... |
| Rule 6. keð..d-Vex | {+$ke,e,+$kð,+ð,-$d,-#d,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-e,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-$ke} | ...+$ke... | 1<k<M-2.
| BI element: | Set Definition: | Possible Patient
| Rule 8. pos | {-$Md},{-d},{-!d} | ...+$Md ...+!d,...+d... |
| Rule 8. neg | {-$Md},{+d},{-!d} | ...+$Md ...+!d,...-d... |
| Rule 8. fail | {$d},{-!d} | ...-$d,...+!d,... |

SCREEN 49. THEOREM 7.

 
THEOREM 7. ÇBICI is d-conative if and only if B0 is d-conative.
Proof: If. If B0 is d-conative, then by Definition 25 (Rule 5), {-$d,+#d,-!d} C B0. By SUBSET COROLLARY, {-$d,+#d,-!d} C B0 c BI c ÇBICI. QED.
Only if: Then t' ~C BH, as follows:

| B0 element: | Set Definition: | Possible Patient
| Rule 2. KwnlOrd$kd/notry | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/fail | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/pos | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KwnlOrd$kd/neg | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KnwlOrd$Me | {-$M-1e,+$Me} | ...-$Me... |
| Rule 2. KnwlOrd$ke | {-$ke,+$k+1e} | ...+$k+1e... | 1<k<M-1
| Rule 3. DataAbs$d/notry | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/fail | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/pos | {+$d,-$Md} | ... +$Md ... |
| Rule 3. DataAbs$d/neg | {+$d,-$Md} | ... +$Md ... |
| Rule 4. d-Hippocr/notry | {-#d,+!d} | ... -!d ... |
| Rule 4. d-Hippocr/fail | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/pos | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/neg | {-#d,+!d} | ... +#d ... |
| Rule 5. d-Conativ/notry | {-$d,+#d,-!d} | ... -#d ... |
| Rule 5. d-Conativ/fail | {-$d,+#d,-!d} | ... +!d ... |
| Rule 5. d-Conativ/pos | {-$d,+#d,-!d} | ... +$d ... |
| Rule 5. d-Conativ/neg | {-$d,+#d,-!d} | ... +$d ... |
| Rule 6. keð..d-Vex | {+$ke,e,+$kð,+ð,-$d,-#d,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-e,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-$ke} | ...+$ke... | 1<k<M-2.
| BI element: | Set Definition: | Possible Patient
| Rule 8. pos | {-$Md},{-d},{-!d} | ...+$Md ...+!d,...+d... |
| Rule 8. neg | {-$Md},{+d},{-!d} | ...+$Md ...+!d,...-d... |
| Rule 8. fail | {$d},{-!d} | ...-$d,...+!d,... |

SCREEN 50. THEOREM 8.

 
THEOREM 8. ÇBICI is keðd-vexative if and only if B0 is keðd-vexative.
Proof: If. By Subset Corollary.
Only if: Then t' ~C BH, as follows:

| B0 element: | Set Definition: | Possible Patient
| Rule 2. KwnlOrd$kd/notry | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/fail | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/pos | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KwnlOrd$kd/neg | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KnwlOrd$Me | {-$M-1e,+$Me} | ...-$Me... |
| Rule 2. KnwlOrd$ke | {-$ke,+$k+1e} | ...+$k+1e... | 1<k<M-1
| Rule 3. DataAbs$d/notry | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/fail | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/pos | {+$d,-$Md} | ... +$Md ... |
| Rule 3. DataAbs$d/neg | {+$d,-$Md} | ... +$Md ... |
| Rule 4. d-Hippocr/notry | {-#d,+!d} | ... -!d ... |
| Rule 4. d-Hippocr/fail | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/pos | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/neg | {-#d,+!d} | ... +#d ... |
| Rule 5. d-Conativ/notry | {-$d,+#d,-!d} | ... -#d ... |
| Rule 5. d-Conativ/fail | {-$d,+#d,-!d} | ... +!d ... |
| Rule 5. d-Conativ/pos | {-$d,+#d,-!d} | ... +$d ... |
| Rule 5. d-Conativ/neg | {-$d,+#d,-!d} | ... +$d ... |
| Rule 6. keð..d-Vex | {+$ke,e,+$kð,+ð,-$d,-#d,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-e,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-$ke} | ...+$ke... | 1<k<M-2.
| BI element: | Set Definition: | Possible Patient
| Rule 8. pos | {-$Md},{-d},{-!d} | ...+$Md ...+!d,...+d... |
| Rule 8. neg | {-$Md},{+d},{-!d} | ...+$Md ...+!d,...-d... |
| Rule 8. fail | {$d},{-!d} | ...-$d,...+!d,... |

SCREEN 51. THEOREM 9.

 
THEOREM 9. ÇBICI is kðe-ontologic if and only if B0 is kðe-ontologic.
Proof: If. By Subset Corollary.
Only if: Then t' ~C BH, as follows:

| B0 element: | Set Definition: | Possible Patient
| Rule 2. KwnlOrd$kd/notry | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/fail | {-$kd,+$k+1d} | ...-$k+1d... | 1<k<M-1
| Rule 2. KwnlOrd$kd/pos | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KwnlOrd$kd/neg | {-$kd,+$k+1d} | ...+$kd... | 1<k<M-1
| Rule 2. KnwlOrd$Me | {-$M-1e,+$Me} | ...-$Me... |
| Rule 2. KnwlOrd$ke | {-$ke,+$k+1e} | ...+$k+1e... | 1<k<M-1
| Rule 3. DataAbs$d/notry | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/fail | {+$d,-$Md} | ... -$d ... |
| Rule 3. DataAbs$d/pos | {+$d,-$Md} | ... +$Md ... |
| Rule 3. DataAbs$d/neg | {+$d,-$Md} | ... +$Md ... |
| Rule 4. d-Hippocr/notry | {-#d,+!d} | ... -!d ... |
| Rule 4. d-Hippocr/fail | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/pos | {-#d,+!d} | ... +#d ... |
| Rule 4. d-Hippocr/neg | {-#d,+!d} | ... +#d ... |
| Rule 5. d-Conativ/notry | {-$d,+#d,-!d} | ... -#d ... |
| Rule 5. d-Conativ/fail | {-$d,+#d,-!d} | ... +!d ... |
| Rule 5. d-Conativ/pos | {-$d,+#d,-!d} | ... +$d ... |
| Rule 5. d-Conativ/neg | {-$d,+#d,-!d} | ... +$d ... |
| Rule 6. keð..d-Vex | {+$ke,e,+$kð,+ð,-$d,-#d,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-e,-$k+1e} | ...+$k+1e... | 1<k<M-2.
| Rule 7. kð..e-Ontol | {+$kð,+ð,-$ke} | ...+$ke... | 1<k<M-2.
| BH element: | Set Definition: | Possible Patient
| Rule 8. pos | {-$Md},{-d},{-!d} | ...+$Md ...+!d,...+d... |
| Rule 8. neg | {-$Md},{+d},{-!d} | ...+$Md ...+!d,...-d... |
| Rule 8. fail | {$d},{-!d} | ...-$d,...+!d,... |

SCREEN 52. THEOREM 10.

THEOREM 10. ñ%ÇBICI is quartic-complete.
Proof: 1. G > &ntlide;F/2 = &ntlide;t, for every t C T; G > H.
2. Sort BI in ascending order, G×log2G steps; index each element in the sorted BI list in F×log2F steps.
3. Climb along BI match to F elements, in F×log2F steps.
4. Perform #3, H times. Total of (G×log2G)3 steps, less than G4 steps, for G>1000.

SCREEN 53. PROSTATE CANCER EXAMPLE 1.

PROSTATE CANCER EXAMPLE 1.
DATA: Ovrsxty. Patient is over sixty, one year since last physical exam.
DATA: Spsa. Serum Prostatic Specific Antigen > 4 ng/dL.
DATA: Prbxca. Prostate biopsy shows adenocarcinoma of prostate.
ENTITY: Prca. Patient has adenocarcinoma of prostate.
RESULT FOR EXAMPLE 1: KNOW1 prca.
DATA FOR EXAMPLE 1: ßOvrsxty.
RESULT FOR EXAMPLE 1: ß1 prca.
Enter data and click on SUBMIT:

TITLE:




      a.      b.     c.     d.     e.     f.     g.     h.     i.      j.     k.     l.      m.     n.
  1.                          
  2.                          
  3.                          
  4.                          
  5.                          
  6.                          
  7.                          
  8.                          
  9.                          
10.                          
11.                          
12.                          
13.                          
14.                          
15.                          
16.                          
17.                          
18.                          
19.                          
20.                          





Modal Logic Solver: http://www.netautopsy.org/modllogc.htm

Modal Logic Solver Source Code: http://www.netautopsy.org/modllprl.htm

SCREEN 54. PROSTATE CANCER EXAMPLE 2.

PROSTATE CANCER EXAMPLE 2.
DATA: Ovrsxty. Patient is over sixty, one year since last physical exam.
DATA: Spsa. Serum Prostatic Specific Antigen > 4 ng/dL.
DATA: Prbxca. Prostate biopsy shows adenocarcinoma of prostate.
ENTITY: Prca. Patient has adenocarcinoma of prostate.
DATA FOR EXAMPLE 2: ßOvrsxty, ßSpsa.
RESULT FOR EXAMPLE 2: ß2 prca.
Enter data and click on SUBMIT:

TITLE:




      a.      b.     c.     d.     e.     f.     g.     h.     i.      j.     k.     l.      m.     n.
  1.                          
  2.                          
  3.                          
  4.                          
  5.                          
  6.                          
  7.                          
  8.                          
  9.                          
10.                          
11.                          
12.                          
13.                          
14.                          
15.                          
16.                          
17.                          
18.                          
19.                          
20.                          





Modal Logic Solver: http://www.netautopsy.org/modllogc.htm

Modal Logic Solver Source Code: http://www.netautopsy.org/modllprl.htm

SCREEN 55. PROSTATE CANCER EXAMPLE 3.

PROSTATE CANCER EXAMPLE 3.
DATA: Ovrsxty. Patient is over sixty, one year since last physical exam.
DATA: Spsa. Serum Prostatic Specific Antigen > 4 ng/dL.
DATA: Prbxca. Prostate biopsy shows adenocarcinoma of prostate.
ENTITY: Prca. Patient has adenocarcinoma of prostate.
DATA FOR EXAMPLE 3: ßOvrsxty, ßSpsa, ßPrbxca.
RESULT FOR EXAMPLE 3: ß3 prca.
Enter data and click on SUBMIT:

TITLE:




      a.      b.     c.     d.     e.     f.     g.     h.     i.      j.     k.     l.      m.     n.
  1.                          
  2.                          
  3.                          
  4.                          
  5.                          
  6.                          
  7.                          
  8.                          
  9.                          
10.                          
11.                          
12.                          
13.                          
14.                          
15.                          
16.                          
17.                          
18.                          
19.                          
20.                          





Modal Logic Solver: http://www.netautopsy.org/modllogc.htm

Modal Logic Solver Source Code: http://www.netautopsy.org/modllprl.htm

Last Updated: October 6, 2003, by G. William Moore, MD, PhD.