# Logic

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.- The Association for Logic Programming (ALP).
- Logic Programming at The WWW Virtual Library.
- logic-programming.org actually empty.
- Formal logic via functional programming: a dissertation.
- Termination inference, a kind of program analysis for logic programs.

- Schelog3 [MIA].
- SPIKE. From its readme:
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.

**Pages in this topic: ** ALF ASF+SDF Axiom of Choice CafeOBJ Claire Curry Curry-Howard Isomorphism Dynamo Escher Goedel Lambda Prolog LIFE Maude Mercury NuPrl Prolog SPARCL TyRuBa Yarrow

**Also linked from: ** Actor Alan Bundy BOBJ Constraints Declarative Fifth Generation Computer Systems Induction and Co-induction Janus NCL OBJ Family Quotienting Referential Transparency and State Scheme Unification