Mercurial > cpdt > repo
diff src/LogicProg.v @ 395:3c941750c347
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 |
line wrap: on
line diff
--- a/src/LogicProg.v Sun Apr 22 15:51:03 2012 -0400 +++ b/src/LogicProg.v Sun Apr 22 16:25:22 2012 -0400 @@ -23,7 +23,7 @@ (** 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. - 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. *) + 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. *) (** * Introducing Logic Programming *)