BussTautology

gapt.examples.BussTautology
object BussTautology

Creates the n-th tautology of a sequence that has only exponential-size cut-free proofs

This sequence is taken from: S. Buss. "Weak Formal Systems and Connections to Computational Complexity". Lecture Notes for a Topics Course, UC Berkeley, 1988, available from: http://www.math.ucsd.edu/~sbuss/ResearchWeb/index.html

Attributes

Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Value members

Concrete methods

def A(i: Int): FOLFormula
def Ant(i: Int): List[FOLFormula]
def B(i: Int): FOLFormula
def F(i: Int): FOLFormula
def apply(n: Int): HOLSequent
def c(i: Int): FOLAtom
def d(i: Int): FOLAtom