-
Notifications
You must be signed in to change notification settings - Fork 18
/
nTape5.scala
56 lines (49 loc) · 2.08 KB
/
nTape5.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
package gapt.examples
import gapt.formats.ClasspathInputFile
import gapt.formats.llk.loadLLK
/**
* Version 5 of the higher-order n-Tape proof, where if-then-else is directly axiomatized i.e. it has 2 additional
* axioms P -> if code(P) then t else f = t and -P -> if code(P) then t else f = f which were theorems before.
* 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.
*/
class nTape5( _size: Int ) extends nTape4( _size ) {
override def proofdb() = loadLLK( ClasspathInputFile( s"ntape/ntape5-$size.llk" ) )
}
/**
* 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.
*/
object nTape5 {
lazy val inst2 = new nTape5( 2 )
lazy val inst3 = new nTape5( 3 )
lazy val inst4 = new nTape5( 4 )
def apply( size: Int ) = size match {
case 2 => inst2
case 3 => inst3
case 4 => inst4
case _ => throw new Exception( "We have only instances 2 to 4." )
}
}
/**
* 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.
*/
class nTape5Arith( _size: Int ) extends nTape4( _size ) {
override def proofdb() = loadLLK( ClasspathInputFile( s"ntape/ntape5-$size-arithmetic-ite.llk" ) )
}
/**
* 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.
*/
object nTape5Arith {
lazy val inst2 = new nTape5Arith( 2 )
def apply( size: Int ) = size match {
case 2 => inst2
case _ => throw new Exception( "We have only instance 2." )
}
}