Logstack
LogStack is a stackbased logic language created by User:Silver. Each item on the stack is a valid sentence of propositional logic, and all conditionals work by popping one and testing whether it can be proven using the rest of the stack as assumptions.
Contents
Instructions
Instruction  Effect 

azAZ  push an atomic proposition corresponding to the letter 
*  push a contradiction 
%  push a tautology 
&  pop two propositions p and q, and push a compound proposition 'p and q' 
  pop two propositions p and q, and push a compound proposition 'p or q' 
!  pop a proposition and push its negation 
^  pop two propositions p and q and push 'p xor q'. This is syntactic sugar, under the hood all compound propositions are in terms of and, or and not 
:  pop two propositions p and q and push 'q implies p' (in that order, so "ab:" pushes a=>b) 
=  pop two propositions p and q and push 'p if and only if q' (biconditional) 
/  swap the top two items on the stack 
;  duplicate the top item on the stack 
$  pop and discard 
@  rotate the stack  pop an proposition and place it on the bottom of the stack 
~  pop a proposition and try to prove it using the rest of the stack. If it is provable, swap the top two items (not replacing the proposition popped for testing) 
?  pop a proposition and try to prove it. output the result ('yes' or 'no') 
()  loop  before each iteration, pop a proposition and try to prove it. If it's not provable, end the loop immediately 
.  halt the program 
#  output the state of the stack, mostly for debugging purposes 
Any other character will be ignored.
Computational Class
LogStack is Turing Complete, as proven by the following translation to 3cell brainfuck:
Brainfuck  LogStack 

+  %

  %/(ab)(%A(%B(C/ab)(Bab)$/ab)(Aab)$ab)$

>  (%@)%A(%B(C/ab)(Bab)$/ab)(Aab)$@

<  (%@)%A(%B(C/ab)(Bab)$/ab)(Aab)$@(%@)%A(%B(C/ab)(Bab)$/ab)(Aab)$@

[  %(%/(

]  %%ab)(%A(%B(C/ab)(Bab)$/ab)(Aab)$abc)$)

Which isn't as ugly as it looks (quite) once you realise that much of it is repeated %A(%B(C/ab)(Bab)$/ab)(Aab)$
, which figures out which of A,B or C have just been popped and pushes the right one back.
Use
As it turns out, the logic part isn't that much use. A subset of the language consisting only of three atomic propositions, %, /, $, @ and () is Turing Complete, as shown above. However, there are a couple of useful things to remember:
 The difference between false and unprovable matters.
p?
on a stack that makes no mention ofp
outputs 'no'.  The principle of explosion applies. If the stack implies a contradiction, all propositions are provable. This breaks the constructions below if it happens.
 the construction
%/( [if true] ab)( [if false] ab)$
acts as an ifelse statement  the construction
*( [comment] )
allows comments
Examples
Truth Machine
Truthy input for this program consists of a starting stack containing a single 'p', falsy input is an empty starting stack.
p *(push (another?) 'p') ( *(pop something, initially the 'p' we just pushed, and try to prove it. If it's not provable, skip past the matching ')') pp?) *(push two 'p's, then pop one of them and output whether or not it's provable  always yes. Then go back to the '(') a? *(push 'a' and output whether it's provable  always no, since it's not mentioned anywhere in the stack)