abella

Interactive theorem prover based on lambda-tree syntax