Mathematical Logic and Programming Languages

ALGOL 60 algorithm ALPHA applied arity ARPANET assertion language axiom system axiomatization behaviour C. A. R. HOARE characterization Clarke Computer Science construct data type declaration defined denoted Dijkstra elements equations execution expression Extension to theory finite interpretations first-order logic fixpoint formula functional language functional programming G₁ gentour given goal Gypsy environment Gypsy software halting problem Hoare axiom Hoare logic Horn clause implementation induction infinite input integer interface introduce learnable lemmas logic programming loop machine Main rules mathematical Milner natural numbers nextmoves notation operator output P₁ pair parameters PARSE positive examples possible predicate calculus procedure programming language properties propositional calculus proved Prvr quicksort recursion relation relatively complete result semantics separated msg_stream x[1..p sequence set theory software engineering software system sound and relatively subset symbol arity tactic Th(I theorem topological sort total correctness tree true University variables verification conditions