Logic Programming is the *(term) for a *(paradigm) of programming that originates in the _(Curry-Howard Isomorphism), which relates types and proofs to terms and expressions. In most cases, logical deduction or inference is equated with term evaluation or state update.

<ul class="links">
<li>_("Logic Programming"|http://www.afm.sbu.ac.uk/logic-prog/) at _("The WWW Virtual Library"|http://www.vlib.org/).</li>
<li>_("Formal logic via functional programming"|http://pauillac.inria.fr/~leifer/research.html#logicreport): a dissertation.</li>
<li>_("Termination inference"|http://www.complang.tuwien.ac.at/cti/), a kind of program analysis for logic programs.</li>
</ul>

<ul class="implementations">
<li>_("Schelog3"|ftp://ftp.cs.rice.edu/public/dorai/schelog3.tar.gz) [_(MIA)].</li>
<li>_("SPIKE"|ftp://ftp.loria.fr/pub/loria/protheo/softwares/Spike/). From its readme:
<blockquote>
The SPIKE system is an automatic theorem prover in theories presented  by conditional equations. SPIKE was written in Caml Light, a functional language of the _(ML) family.
<blockquote>
</li>
</ul>
