Value Members

1.  val proofSequences: Seq[ProofSequence]
2.  object BussTautology

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

   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

3.  object CASCData
4.  object CASCEvaluation
5.  object CERESExpansionExampleProof
6.  object CountingEquivalence

   Sequence of valid first-order formulas about equivalent counting methods.

   Sequence of valid first-order formulas about equivalent counting methods.

   Consider the formula ∀z ∃⁼¹i ∀x ∃y a_i(x,y,z), where ∃⁼¹i is a quantifier that says that there exists exactly one i (in 0..n) such that ∀x ∃y a_i(x,y,z) is true.

   This function returns the equivalence between two implementations of the formula: first, using a naive quadratic implementation; and second, using an O(n*log(n)) implementation with threshold formulas.

7.  object ECSJumpSchema extends TacticsProof
8.  object EventuallyConstantSchema extends TacticsProof
9.  object EventuallyConstantSchemaInductionRefutation extends TacticsProof
10.  object EventuallyConstantSchemaRefutation extends TacticsProof
11.  object ExponentialCompression extends TacticsProof
12.  object FirstSchema0 extends TacticsProof
13.  object FirstSchema1 extends TacticsProof
14.  object FirstSchema2 extends TacticsProof
15.  object FirstSchema3 extends TacticsProof
16.  object FirstSchema4 extends TacticsProof
17.  object FirstSchema5 extends TacticsProof
18.  object FirstSchema6 extends TacticsProof
19.  object FirstSchema7 extends TacticsProof
20.  object FirstSchema8 extends TacticsProof
21.  object FirstSchema9 extends TacticsProof
22.  object Formulas

    Contains some commonly used formulas.

23.  object FourStrictMonotoneSchema extends TacticsProof
24.  object FunctionIterationRefutation extends TacticsProof
25.  object FunctionIterationRefutationPos extends TacticsProof
26.  object FunctionIterationSchema extends TacticsProof
27.  object GradedStrictMonotoneSchema extends TacticsProof
28.  object GradedStrictMonotoneSequenceRefutation extends TacticsProof
29.  object GradedStrictMonotoneSequenceSchema extends TacticsProof
30.  object MonoidCancellation extends TacticsProof

    Monoid cancellation benchmark from Gregory Malecha and Jesper Bengtson: Extensible and Efficient Automation Through Reflective Tactics, ESOP 2016.

31.  object NdiffSchema extends TacticsProof
32.  object NiaSchema extends TacticsProof
33.  object NiaSchemaRefutation extends TacticsProof
34.  object OneStrictMonotoneRefutation extends TacticsProof
35.  object OneStrictMonotoneSchema extends TacticsProof
36.  object OneStrictMonotoneSequenceRefutation extends TacticsProof
37.  object OneStrictMonotoneSequenceSchema extends TacticsProof
38.  object PQPairs

    Creates the n-th formula of a sequence where distributivity-based algorithm produces only exponential CNFs.

39.  object Permutations

    Given n >= 2 creates an unsatisfiable first-order clause set based on a statement about the permutations in S_n.

40.  object Pi2Pigeonhole extends TacticsProof
41.  object Pi3Pigeonhole extends TacticsProof
42.  object PigeonHolePrinciple

    Constructs a formula representing the pigeon hole principle.

    Constructs a formula representing the pigeon hole principle. More precisely: PigeonHolePrinciple( p, h ) states that if p pigeons are put into h holes then there is a hole which contains two pigeons. PigeonHolePrinciple( p, h ) is a tautology iff p > h.

    Since we want to avoid empty disjunctions, we assume > 1 pigeons.

43.  object ReductionDemo extends Script
44.  object ReforestDemo extends Script
45.  object SimpleMutualInductionSchema extends TacticsProof
46.  object StrictMonotoneSchema extends TacticsProof
47.  object StrongStrictMonotoneSchema extends TacticsProof
48.  object ThreeStrictMonotoneRefutation extends TacticsProof
49.  object ThreeStrictMonotoneSchema extends TacticsProof
50.  object TwoStrictMonotoneRefutation extends TacticsProof
51.  object TwoStrictMonotoneSchema extends TacticsProof
52.  object VeryWeakLexicoPHPSchema extends TacticsProof
53.  object VeryWeakLexicoPHPSchemaVariant extends TacticsProof
54.  object VeryWeakLexicoPHPSchemaVariantRefutation extends TacticsProof
55.  object VeryWeakPHPSeqSchema extends TacticsProof
56.  object VeryWeakPHPSeqTwoSchema extends TacticsProof
57.  object VeryWeakPHPSequenceVariantSchema extends TacticsProof
58.  object divisionByTwo extends TacticsProof
59.  object drinker extends TacticsProof
60.  object elemAtIndex extends TacticsProof
61.  object epsilon extends Script
62.  object fol1 extends TacticsProof
63.  object fol2

    Provides a simple intuitionistic proof of ¬p ∨ p ⊢ ¬¬p → p.

    Provides a simple intuitionistic proof of ¬p ∨ p ⊢ ¬¬p → p. Applying the CERES method will create a non-intuitionistic proof but reductive cut-elimination will always create an intuitionistic one. Therefore this is an example that CERES produces cut-free proofs which reductive cut-elimination cannot.

64.  object gapticExamples
65.  object gniaSchema extends TacticsProof
66.  object implicationLeftMacro
67.  object instprover extends Script
68.  object lattice extends TacticsProof
69.  object nTape2 extends nTape2
70.  object nTape3 extends nTape3
71.  object nTape4
72.  object nTape5

    Version 5 of the higher-order n-Tape proof.

    Version 5 of the higher-order n-Tape proof. In contrast to nTape4 it cuts on instances of the theorem C for specific upper bounds n. Since the instantiated proofs were generated manually, only nTape5(2) to nTape5(4) work.

73.  object nTape5Arith

    Version 5 of the higher-order n-Tape proof, where if-then-else is still proved in arithmetic.

    Version 5 of the higher-order n-Tape proof, where if-then-else is still proved in arithmetic. In contrast to nTape4 it cuts on instances of the theorem C for specific upper bounds n. Since the instantiated proofs were generated manually, only nTape5Arith(2) works.

74.  object nTape6

    The object nTape6 generates hard problems for higher order theorem provers containing an axiomatization of if-then-else.

    The object nTape6 generates hard problems for higher order theorem provers containing an axiomatization of if-then-else. Formulas: f1,f2 ... if-then-else axiomatizations f3,f4 ... properties of the successor function (0 is no successor and a number is always different from its successor) conclusion0 ... there exists a function h s.t. h(0) = 1, h(1) = 0 conclusion1 ... there exists a function h s.t. h(0) = 1, h(1) = 0, h(2) = 0 conclusion2 ... there exists a function h s.t. h(0) = 1, h(1) = 0, h(2) = 1 w1 ... witness for sc w2 ... witness for sc2

    The problems are (in sequent notation):

    P0: f1, f2 :- conclusion0 P1: f1, f2, f3, f4 :- conclusion1 P2: f1, f2, f3, f4 :- conclusion2

    The generated filenames are "ntape6-i-without-witness.tptp" for i = 0 to 2.

    To show that there are actual witnesses for the function h, we provide a witness, where the witness w1 can be used for both W0 and W1:

    W0: { w1 :- } x P0 W1: { w1 :- } x P1 W2: { w2 :- } x P2

    The generated filenames are "ntape6-i-with-witness.tptp" for i = 0 to 2.

75.  object nTapeInstances
76.  object philsci
77.  object primediv extends TacticsProof
78.  object successor extends TacticsProof
79.  object tape extends TacticsProof
80.  object tapeUrban extends TacticsProof

    Formalisation of the tape-proof as described in C.

    Formalisation of the tape-proof as described in C. Urban: Classical Logic and Computation, PhD Thesis, Cambridge University, 2000.

81.  object tautSchema extends TacticsProof
82.  object tbillc extends TacticsProof

    This is an example used in the talk[1] at TbiLLC 2013.

    This is an example used in the talk[1] at TbiLLC 2013. It generates a (cut-free) LK proof where the extracted expansion tree has nested quantifiers.

    [1] http://www.illc.uva.nl/Tbilisi/Tbilisi2013/uploaded_files/inlineitem/riener.pdf