- Halting problem for the call-by-value lambda-calculus HaltL
- Halting problem for multi-tape and single-tape Turing machines HaltMTM and HaltTM 1
- Halting problem for simple binary single-tape Turing machines HaltSBTM
- Basics of decision problems
- Time Hierarchy theorem
- Comparison of techniques for deriving resource bounds we explored
- Explicit Bounds
- Intuitive Bounds using upToC
- A mixed approach (this is the one currently used in the SAT file)
- PrettyBounds for LM
- Computability in L
- Derivation of the pigeonhole principle on lists
- Uniform homomorphisms
- Various preliminaries for the TM -> SAT part of the Cook-Levin Theorem
- Representation of finite types by natural numbers
- Clique on flat graphs and NP containment
- Flat representation of an undirected graph.
- Reduction from k-SAT to Clique
- k-SAT to FlatClique
- Plain undirected graphs
- The hardness proof of GenNP is prettier
- Overview of the results proved in the paper.
- Shared Definitions for SAT and FSAT
- SAT: Satisfiability of CNFs
- k-SAT
- Formula Satisfiability: the satisfiability problem on arbitrary Boolean formulas
- Some generic tools for encoding things as Boolean formulas
- FSAT to SAT via Tseytin transformation
- Reduction of TMGenNP with fixed TM to TMGenNP with variable TM
- Adding preludes to P-3-CC instances
- extraction of the reduction from FlatGenNP to FlatCC
- Reduction of 3-CC to CC.
- Reduction of FlatTCC to FlatCC
- Results on the behaviour of CC under string homomorphisms
- CC to BinaryCC
- Reduction of FlatCC to BinaryCC
- Reduction of single-tape Turing machines to 3-CC
- Alphabet
- Representation of tapes
- Representation of configurations
- Automation for discrimination of the tape relation
- Inductive rules for tape coverings
- Changing tape representations by one symbol
- Transition rules
- Halting rules
- Combined rules for the simulation of Turing machines
- A few simple facts about applicability of rules
- A few more technical facts regarding coverings
- Automation for the simulation proofs
- multi-step simulation
- nondeterministic guessing of input
- list-based cards
- agreement for transitions
- Reduction of BinaryCC to FSAT
- Flat Covering Cards
- Flat 3-Covering Cards
- BinaryCC: Parallel Rewriting restricted to a binary alphabet
- Covering Cards
- 3-Covering Cards
- Simpler definitions for single-tape Turing machines.
- Definition of a generic problem for single-tape Turing machines
- From L to TMs
- This start might be bad, as we need to check the bound explicitly, e.g. count the beta-steps during the simulation.
- But we can choose the bound large enough such that the term we simulate halts in the bound or always diverges
- We might want to simulate some L term that always halts
- But that means we need to distinguish true/false in the representation.
- Eventuell moechten wir nicht mit einem "einfachen" problem starten, sondern erst eienn lambda-trm scheiben, der decider für eine lang genuge zeit simulirt und dann hält oder divergiert, je nachdem ob der Decider wahr oder falsch sagt
- Divergenz ist ein schlechter Problem, wenn man von divergens reduziert, da man häufig nur obere schranken für die Laufzeit der Simulatoren hat.
- Definitions and Automation for PrettyBounds
- Automation
- PrettyBounds for Machines in TM/Code
- PrettyBound for Univ
- Bounds For M2M
- Case Study: Place usage for list machines
- Space Analysis for Univ
- Theorem: Univ can simulate multi-tape Turing machines with polynominal time and linear space overhead