- Basics of decision problems
- Overview over the results proved in the thesis
- #P (verifier characterisation)
- Representation of finite types by natural numbers
- Shared Definitions for SAT and FSAT
- SAT: Satisfiability of CNFs
- k-SAT
- Plain undirected graphs
- Flat representation of an undirected graph.
- Clique on flat graphs and NP containment
- Derivation of the pigeonhole principle on lists
- Reduction from k-SAT to Clique
- k-SAT to FlatClique
- Definition of a generic NP-hard problem
- Reduction of GenNP with fixed TM to GenNP with variable TM
- Simpler definitions for single-tape Turing machines.
- Parallel Rewriting
- 3-Parallel Rewriting
- Adding preludes to P-3-PR instances
- Reduction of single-tape Turing machines to 3-PR
- Alphabet
- Representation of tapes
- Representation of configurations
- Automation for discrimination of the tape relation
- Inductive rules for tape rewrites
- The following results generalise Lemma 16 -17 to arbitrary tapes
- Transitions
- Predicate for halting extensions
- Combined rules for the simulation of Turing machines
- A few simple facts about applicability of rules
- A few more technical facts regarding rewrites
- Automation for the simulation proofs
- multi-step simulation
- nondeterministic guessing of input
- list-based windows
- agreement for transitions
- Flat Parallel Rewriting
- Flat 3-Parallel Rewriting
- extraction of the reduction from FlatGenNP to FlatPR
- Uniform homomorphisms
- Results on the behaviour of PR under string homomorphisms
- BinaryPR: Parallel Rewriting restricted to a binary alphabet
- PR to BinaryPR
- Formula Satisfiability: the satisfiability problem on arbitrary Boolean formulas
- Reduction of BinaryPR to FSAT
- FSAT to SAT via Tseytin transformation
- The hardness proof of GewnNPHalt is prettier
- Resource Measures
- Time Hierarchy theorem
- Preliminaries
- Shared libraries
- Finitary sums and products over monoids
- Binomial theorem
- Bitwise operations on nat as list bool
- Bitwise operations on nat
- Euclidian division and Bezout's identity
- Prime numbers
- Base p representation
- Reification for bounded quantification
- Pidgeon hole principle
- Iteration of binary relations
- Traditional Definition
- Inductive Definition
- Binary PCP
- Binary Post correspondence problem with indices
- Decidability and Enumerability
- Many-One Reductions
- Post's Theorem and Markov's Principle
- Post Correspondence Problem
- First-Order Logic
- Tarski Semantics
- Natural Deduction
- Kripke Semantics
- FOL Reductions
- Intuitionistic FOL
- Classical Natural Deduction
- Weakening
- Infinite Data Types
- Definitions
- SRH to SR
- SR to MPCP
- MPCP to PCP
- PCP to CFP
- PCP to CFI
- TM to SRH
- Post grammars are context-free
- CFP to CFI
- Code
- A certified low-level compiler
- Binary Stack Machines
- Minsky Machines
- Intuionistic Linear Logic
- List of all results
- Formal Undecidability
- Alternate Minsky Machines such that two counters are enough for undec
- Minsky machines to FRACTRAN programs
- Arithmetic libraries for Matiyasevich's theorems
- Object-level representation of Diophantine equations
- Diophantine logic
- Elementary diophantine constraints
- Single Diophantine equations
- Object-level encoding of exponential
- Object-level encoding of bounded universal quantification I
- Object-level encoding of bounded universal quantification II
- Object-level encoding of bounded universal quantification III
- Reflexive transitive closure is Diophantine
- FRACTRAN termination is Diophantine
- Main undecidability results and DPRM theorem
- Basis for the full TM library
- Relations
- Definition of Multi-Tape Turing Machines
- 0-tape Turing machine that does nothing.
- Basic 1-Tape Machines
- Primitive Two-tape machines
- Combinators
- Switch Combinator
- Mirror Operator
- Tapes-Lift
- Tactic Support
- Alphabet-Lift
- Tactics that help verifying complex machines
- Simple compound multi-tape Machines
- Move to a symbol and translate read symbols
- Copy Symbols from t0 to t1
- Compare two tapes (from left to right) until a symbol is reached
- Codable Class
- Value-Containing
- Alphabet-lift for "programmed" Turing Machines
- Copying Machines and Helper functions for verifying machines using CopySymbols ane MoveToSymbol
- Compare two values
- All tools for programming Turing machines
- Constructor and Deconstructor Machines for Natural Numbers
- Constructor and Deconstructor Machines for Sum Types and Option Types
- Constructor and Deconstructor Machines for Lists
- Constructors and Deconstructors for Finite Types
- Constructors and Deconstructors for Bool
- Constructors and Deconstructors for Pair Types
- Machines that compte natural functions
- Machines that compute list functions
- Encoding for binary numbers
- Pointer bookkeeping for machines using (positive) binary numbers
- Machine for comparing two positive binary numbers
- Machines for shifting positive binary numbers
- Multiplication of positive numbers
- Machines on N (binary natural numbers)
- Lookup an entry in an associative list
- Universal Turing Machine
- Definitions and Automation for PrettyBounds
- Automation
- Maximum element in a list
- 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
- Preliminaries
- The call-by-value lambda calculus L
- Correctness and time bounds
- Certifying extraction from Coq to L with time bounds
- Encodings and extracted basic functions
- Extracted Functions
- Extracted equality of encoded natural numbers
- Extracted equality of encoded terms
- Extracted encoding of natural numbers
- Extracted term encoding
- Extracted tuple encoding
- Decidabiity of closedness, boundedness and procness
- Extracted size of terms
- Extracted substitution on terms
- Extracted step-indexed L-interpreter
- Computability of full evaluation
- Enumeratibility of L-terms
- Computability of Ackermann
- Extraction of Turing Machine interpreter
- unflatten Tapes
- unflatten Conf
- Reducing halting problem for TMs to halting problem for L
- Diophantine Equations
- Computability in L
- Abstract L machines
- Semantics of the Heap Machine
- Definition of L-acceptability
- Properties of acceptance
- L-acceptable predicates are closed under conjunction and disjunction
- L-ecidable predicates are L-acceptable (and their complement too)
- Definition of L-decidability
- Complement, conj and disj of predicates
- Deciders for complement, conj and disj of ldec predicates
- L-decidable predicates are closed under complement, conj and disj
- First Fixed Point Theorem
- Second Fixed Point Theorem
- Definition of parallel or
- The self halting problem is not L-acceptable
- Rice's Theorem
- Applications of Rice's Theorem
- Rice's Theorem, classical, on combinators
- Scott's Theorem
- Applications of Scott's Theorem
- Step indexed evaluation
- Alphabets
- Constructors and Deconstructors for Comens
- Heap Lookup
- Implementation of ϕ (aka SplitBody)
- Step Machine of the Heap Machine Simulator
- Reduction of the Halting Problem of the Heap Machine to the Halting Problem of Turing Machines
- PrettyBounds for LM
- L to TM