Bell Labs logo

A Tale of Two Logics, Three Systems, Four Languages, and Fifteen Years


by Peter F. Patel-Schneider

Abstract

I have been involved in the design and implementation of reasoners for (almost) fifteen years. During this time I have had the mixed fortune to have implemented three systems for two very different sorts of logics in three programming languages (plus an attempt using a fourth language). In this talk I will describe some of this work and expound on the lessons I (painfully) learned. Some of these lessons were quite a surprise to me; others run counter to the perceived management wisdom of the time.

This work has been carried out with a number of colleagues, most notably

This talk was given as an invited talk at the IJCAR-2001 Workshop on Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics. Sienna, Italy, June 2001.

History

Logics:
inexpressive, expressive
Systems:
CLASSIC, NeoClassic,, DLP
Languages:
Lisp, C++, Java, ML
Years:
  • 1986-1988 - Kandor (maintenance)
  • 1989-1994 - CLASSIC
  • 1994-1997 - NeoClassic
  • 1998-2001 - DLP

CLASSIC

The Language of CLASSIC

<concept-expression> ::= THING | CLASSIC-THING
  | HOST-THING | <concept-name>
  | (AND <concept-expression>+)
  | (ALL <role-name> <concept-expression>)
  | (ATLEAST <positive-integer> <role-name>)
  | (ATMOST <positive-integer> <role-name>)
  | (FILLS <role-name> <individual-name>+
  | (SAMEAS <attribute-path> <attribute-path>)
  | (TESTC <function> <arg>*
  | (TESTH <function> <arg>*
  | (ONEOF <individual-name>)
  | (MAX <number>)
  | (MIN <number>)
<individual-expression> ::= <concept-expression>
<rule> ::= (<concept-name> <concept-expression>)

NeoClassic

Experiences from CLASSIC and NeoClassic

DLP

The (A) Language of DLP

Concepts <concept name>
  TOP
  BOTTOM
  NUMBER
  STRING
  (NOT <concept>)
  (AND <concept>+)
  (OR <concept>+)
  (SOME <role> <concept>)
  (ALL <role> <concept>)
  (ATLEAST <n> <concept>)
  (ATMOST <n> <concept>)
Roles <role name>
Roles can be defined to be transitive.

Main Optimizations in DLP

Normalisation
  • transform into a normalised form
  • perform simplifications
BCP
look for places with only one choice and perform them first
Semantic Branching
pick a ``variable'' and assign it to true or false, instead of picking a disjunction and assigning a disjunct to true
Backjumping
when backtracking skip over choices that did not contribute to the failure
Caching
remember and reuse results of modal sub-problems
Heuristics
heuristics to enhance backjumping or BCP

Effects of Optimizations

Total Tableaux'98 problems solved

Optimisation Removed Oldest-random Oldest-JW JW Random
NONE 967 915 936 874
Caching 882 826 851 671
Backjumping 880 847 877 795
Semantic Branching 849 --- --- 851
BCP 932 873 879 839
Normalisation 911 913 931 781

Effects of Optimizations

Provable S4 Tableaux'98 problems solved

Optimisation Removed Heuristic 45 branch grz ipc md path ph s5 t4p
NONE Oldest-random 21 18 21 10 3 15 7 21 21
Oldest-JW 21 21 21 10 3 8 5 21 21
JW 21 18 21 10 3 9 5 21 21
Random 21 18 21 21 4 7 7 21 21
Caching Oldest-random 21 18 21 8 7 8 7 21 21
Oldest-JW 21 21 21 7 7 5 5 10 21
JW 21 18 21 7 7 6 5 21 21
Random 21 18 0 13 4 3 7 21 21
Backjumping Oldest-random 21 17 21 9 3 3 7 2 21
Oldest-JW 21 21 21 9 3 3 4 2 18
JW 21 17 21 9 3 3 4 4 21
Random 21 17 21 8 3 3 5 4 21
Semantic Branching Oldest-random 15 18 21 7 3 3 7 4 7
Random 15 18 21 7 3 3 7 4 7
BCP Oldest-random 21 15 21 10 3 11 6 21 21
Oldest-JW 21 21 21 10 3 7 4 15 21
JW 21 12 21 10 3 8 4 21 21
Random 21 16 21 21 4 7 6 21 21
Normalisation Oldest-random 21 18 7 10 3 9 6 21 21
Oldest-JW 21 21 21 10 3 10 6 21 21
JW 21 16 21 10 3 9 6 21 21
Random 21 10 21 21 4 7 7 4 21

Effects of Optimizations

Classification times for Galen knowledge base (CPU seconds)

Optimisation Removed Oldest-random Oldest-JW JW Random
NONE 70 172 153 37
Caching 399 1182 1005 326
Backjumping >10,000 >10,000 >10,000 >10,000
Semantic Branching 2087 --- --- 319
BCP 90 431 616 40
Normalisation 87 207 162 39

Effects of Optimizations

Comparisons with older systems:
Median Solution times for PS12 Formulae
Median Solution times for PS13 Formulae

Comparisons between optimizations:
Solution times for K-dum-n
Solution times for S4-s5-p
Median solution times for PS12 formulae
90th percentile solution times for PS12 formulae

Experiences from DLP

Lessons

Surprises

Facts

Management Wisdom

Use accepted practices

Most Important Lesson

Building a new reasoner is an exploration