Formulas as Programs. Probability, Networks and Algorithms

摘要

The authors provide here a computational interpretation of first-order logic211u001ebased on a constructive interpretation of satisfiability w.r.t. a fixed but 211u001earbitrary interpretation. In this approach the formulas themselves are programs. 211u001eThis contrasts with the so-called formulas as types approach in which the proofs 211u001eof the formulas are typed terms that can be taken as programs. This view of 211u001ecomputing is inspired by logic programming and constraint logic programming but 211u001ediffers from them in a number of crucial aspects. Formulas as programs is argued 211u001eAlma-0 Apt, Brunekree, Partington and Schaerf (1998) that combines the advantages 211u001eof imperative and logic programming. The work here reported can also be used to 211u001ereason about the correctness of on-recursive Alma-0 programs that do not include 211u001edestructive assignment.