## Logic from Computer Science: Proceedings of a Workshop Held November 13 - 17, 1989 [at MSRI]The volume is the outgrowth of a workshop with the same title held at MSRI in the week of November 13-17, 1989, and for those who did not get it, Logic from Computer Science is the converse of Logic in Computer Science, the full name of the highly successful annual LICS conferences. We meant to have a conference which would bring together the LICS commu nity with some of the more traditional "mathematical logicians" and where the emphasis would be on the flow of ideas from computer science to logic rather than the other way around. In a LICS talk, sometimes, the speaker presents a perfectly good theorem about (say) the A-calculus or finite model theory in terms of its potential applications rather than its (often more ob vious) intrinsic, foundational interest and intricate proof. This is not meant to be a criticism; the LICS meetings are, after all, organized by the IEEE Computer Society. We thought, for once, it would be fun to see what we would get if we asked the speakers to emphasize the relevance of their work for logic rather than computer science and to point out what is involved in the proofs. I think, mostly, it worked. In any case, the group of people represented as broad a selection of logicians as I have seen in recent years, and the quality of the talks was (in my view) exceptionally, unusually high. I learned a lot and (I think) others did too. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

II | 1 |

III | 17 |

IV | 51 |

V | 73 |

VI | 95 |

VII | 129 |

VIII | 153 |

IX | 217 |

XIV | 319 |

XV | 359 |

XVI | 373 |

XVII | 387 |

XVIII | 405 |

XIX | 481 |

XX | 499 |

XXI | 521 |

### Common terms and phrases

3-valued algebra algorithm applied arithmetic automaton axioms bounded built-in predicates calculus clause closed world assumption complete computational game Computer Science consistent construction contains corresponding countable defined definition denote dinatural equations equivalent example execution extended finite first-order formula function symbols functors game tree given grammar hence Herbrand models higher-order unification induction infinite input interpretation intuitionistic intuitionistic logic isomorphic Kleene Kripke model Lemma logic programming Mathematics models of comp(P morphisms natural deduction natural numbers natural transformations negation as failure normal form operator oracle pair paramodulation parse partial evaluator phrase plays polynomial position problem programming language Prolog proof system propositional provable prove QL^X quantifiers query recursive functions relation restricted result rewrite rules satisfy second-order logic semantics sentences sequence SLDNF-resolution SOL(Comp0 strategies string structure substitution subtree Suppose Temporal Logic termination Theorem theory tion topos unification unifier University