Using a Theorem Prover in the Design of Organic Syntheses
Tunghwa Wang, Ilene Burnstein, Michael Corbett, Steven Ehrlich, Martha W. Evens, Alice Gough, Peter Johnson · ACS symposium series · 1986
This paper describes an expert system for organic synthesis which uses a resolution based theorem prover as its reasoning component. This reasoning component is built upon LMA (Logic Machine Architecture), a collection of Pascal subroutines written by the theorem proving group at Argonne National Laboratory. The SYNLMA system (SYNthesis with LMA) represents the target compound as a theorem to be proved, while the starting materials and reaction rules become axioms. The main advantages of SYNLMA stem from the independence of the database from the inferencing mechanism. This separation makes it possible to experiment with different representations of knowledge and different data bases, like the large chemical databases made available by ISI and Chemical Abstracts, without reprogramming.