Intensional Logics for ProgrammingLuis Fariñas del Cerro, Martti Penttonen Intensional logics provide a comprehensive theoretical basis for establishing the foundations of programming. This volume offers seminal work on the use of intensional logics for the semantic analysis of logic programs, and programming in intensional logics. For example, modal logic, temporal logic, and linear logic prove to be very useful for these purposes. The work presented here thus yields a better understanding of logic programs and will have a significant impact on future developments of logic programming languages. The book will interest computer science graduate students and researchers, particularly those concerned with artificial intelligence, knowledge representation, logic programming, expert systems, reasoning, and natural languages. |
Contents
Monotone logic programming | 1 |
Theory and practice of temporal | 27 |
A simple proof of the completeness | 51 |
Copyright | |
3 other sections not shown
Common terms and phrases
abstract logic allowed answer substitution atomic formula axioms B₁ choice predicates CHRONOLOG classical logic classical logic programming Computer Science connectives D-formula daughter labelled declarative semantics defeasible logics defeasible rules defeasible theory defined Definition denote derivable element example extend finitely failed first-order function symbols goal G ground term Herbrand base Herbrand interpretation Horn clause Horn clause fragment implementation induction inference rule Lang(P LComp(P least fixpoint Lemma linear logic literal logic pro Lwff metalanguage modal logic modulo N₁ negation as failure next-atom node non-classical logics notion philosopher Pr+.Pr predicate calculus predicate logic predicate symbols program clause PROLOG proof tree properties Proposition provable quantifiers realizable w.r.t. refutation satisfies semantics of logic sequent SLDNF subset t₁ TEMPLOG program temporal Herbrand interpretation temporal Herbrand model temporal interpretation temporal logic program temporal operators Theorem three-valued true TSLD-resolution