Mercurial > cpdt > repo

comparison src/LogicProg.v @ 395:3c941750c347

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Citations for lazy data structures, Haskell 'deriving', and logic programming
author Adam Chlipala <adam@chlipala.net>
date Sun, 22 Apr 2012 16:25:22 -0400
parents d1276004eec9
children 05efde66559d
comparison
equal deleted inserted replaced
394:cc8d0503619f 395:3c941750c347
21 21
22 \chapter{Proof Search by Logic Programming}% *) 22 \chapter{Proof Search by Logic Programming}% *)
23 23
24 (** The Curry-Howard correspondence tells us that proving is %``%#"#just#"#%''% programming, but the pragmatics of the two activities are very different. Generally we care about properties of a program besides its type, but the same is not true about proofs. Any proof of a theorem will do just as well. As a result, automated proof search is conceptually simpler than automated programming. 24 (** The Curry-Howard correspondence tells us that proving is %``%#"#just#"#%''% programming, but the pragmatics of the two activities are very different. Generally we care about properties of a program besides its type, but the same is not true about proofs. Any proof of a theorem will do just as well. As a result, automated proof search is conceptually simpler than automated programming.
25 25
26 The paradigm of %\index{logic programming}%logic programming, as embodied in languages like %\index{Prolog}%Prolog, is a good match for proof search in higher-order logic. This chapter introduces the details, attempting to avoid any dependence on past logic programming experience. *) 26 The paradigm of %\index{logic programming}%logic programming%~\cite{LogicProgramming}%, as embodied in languages like %\index{Prolog}%Prolog%~\cite{Prolog}%, is a good match for proof search in higher-order logic. This chapter introduces the details, attempting to avoid any dependence on past logic programming experience. *)
27 27
28 28
29 (** * Introducing Logic Programming *) 29 (** * Introducing Logic Programming *)
30 30
31 (** Recall the definition of addition from the standard library. *) 31 (** Recall the definition of addition from the standard library. *)