Logic as Programming

Abstract

Starting from a general dynamic analysis of reasoning and programming, we develop two main dynamic perspectives upon logic programming. First, the standard fixed point semantics for Horn clause programs naturally supports imperative programming styles. Next, we provide axiomatizations for Prolog-type inference engines using calculi of sequents employing modified versions of standard structural rules such as monotonicity or permutation. Finally, we discuss the implications of all this for a broader enterprise of ‘abstract proof theory’.