This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Algorithmic State Machine Design and Automatic Theorem Proving: Two Dual Approaches to the Same Activity
October 1986 (vol. 35 no. 10)
pp. 853-861
D. Snyers, Philips Research Laboratory
This paper shows that synthesizing binary decision programs (formed by means of decision instructions of the type if then else and of execution instructions of the type do) and proving theorems can be carried out by using the same approach. It is proved that the same transformations acting on P-functions can be interpreted in terms of binary program synthesis and of theorem proving. Since binary program leads to algorithmic state machine design while theorem proving leads to declarative programming, this allows us to lay a bridge between logic design and declarative languages such as Prolog.
Index Terms:
switching theory, Algorithmic state machine, automatic theorem proving, declarative languages, implementation of algorithms, logic, P-functions, resolution principle
Citation:
D. Snyers, A. Thayse, "Algorithmic State Machine Design and Automatic Theorem Proving: Two Dual Approaches to the Same Activity," IEEE Transactions on Computers, vol. 35, no. 10, pp. 853-861, Oct. 1986, doi:10.1109/TC.1986.1676676
Usage of this product signifies your acceptance of the Terms of Use.