judge-0.1.3.0: formulas.txt

##############################################################################
# This file contains some example formulas to try                            #
##############################################################################

# A simple propositional test
(~r -> p) & (r -> q) -> (p | q)

# The Application axiom should derive instantly in both J0 and J0-PB
x:A → y:(A → B) → y*x:B

# ... and this one should fail instantly
x:A → y:(A → B) → x*y:B

# Using proof checker, should work only in LP
x:a → y:(x:a → b) → y·!x:b

# This is a good one: it works in both J0 and J0-PB, but inspects about 
# 18000 formulas in the latter (or 8000 if x:A is in the CS instead of the
# antecedent)
x:A → y:(A → B) → y*(x+x'):B

# ... and this one just gets too complex to find at all
x:A → y:(A → B) → (y+y')*x:B