Analytic Tableaux for Simple Type Theory and its First-Order Fragment

Chad E. Brown, Gert Smolka

We study simple type theory with primitive equality (STT) and its first-order fragment EFO, which restricts equality and quantification to base types but retains lambda abstraction…