El presente trabajo es una lectura de la obra jurídica de Michele Taruffo desde la teoría y la filosofía del derecho. Consiste en reconstruir la obra del profesor lombardo, dispersa a lo largo de cinco décadas, no como un sistema de derecho procesal o una línea de monografías coherente -que serían lecturas posibles-, sino como una teoría de la decisión judicial, a partir de dos ejes cardinales que son recurrentes en sus trabajos: el concepto de motivación de la sentencia y el concepto de prueba. Para ello, la investigación parte de describir el marco de las principales influencias teóricas en la formación del profesor de la Universidad de Pavía, desde tres perspectivas: la del procesalismo italiano, la de la iusfilosofía analítica y la de un conjunto heterogéneo de autores, desde comparatistas a teóricos, con los que se cruzó la obra de Taruffo. La parte propositiva consiste en reconstruir aquello en lo que consiste la obra fundamental del autor: el concepto de jurisdicción, el concepto de decisión judicial que se deriva del primero, y el concepto de prueba. El primero supone una lectura -en clave de “alta dogmática”- de la actividad consistente en resolver controversias y de los presupuestos de su legitimidad. El segundo redescubre la funcionalidad de la motivación de la sentencia judicial desde las razones por las que se exige en los ordenamientos modernos. El tercero se concentra en la racionalidad subyacente a la búsqueda (de la fijación) de la verdad en las premisas que integran el discurso justificativo de las decisiones judiciales.

In this thesis we see deductive systems for classical propositional and predicate logic which use deep inference, i.e. inference rules apply arbitrarily deep inside formulas, and a certain symmetry, which provides an involution on derivations. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they enjoy various new interesting properties. Not only the identity axiom, but also cut, weakening and even contraction are reducible to atomic form. This leads to inference rules that are local, meaning that the effort of applying them is bounded, and finitary, meaning that, given a conclusion, there is only a finite number of premises to choose from. The systems also enjoy new normal forms for derivations and, in the propositional case, a cut elimination procedure that is drastically simpler than the ones for sequent systems.

This thesis will cover an elementary proof of the Riemann–Roch Theorem for planecurves. We will introduce the notions of divisors, which is a convenient way of com-puting multiplicities of rational function, then continuing by introducing differentials.Furthermore we will introduce the K-vector space L(D), consisting of rational func-tions which are controlled by a divisor D. This is followed by presenting some moreresults before we arrive at an elementary proof of the Riemann–Roch Theorem.

The requirements of privacy have become a necessity in modern-day internet-based applications. This applies from traditional client-server applications to blockchain-based applications. Blockchains being a new domain for application development, the priority towards privacy beyond pseudo anonymity has been lacking. With financial applications built on blockchains entering mainstream adoption, and these applications handling sensitive data of users, it is useful to be able to understand how privacy technologies can help in ensuring that the user’s data privacy is maintained. This project addresses this by taking a simple financial transaction use case and applying various privacy technologies like Data Encryption, Zero-Knowledge Proofs, Trusted Execution Environments. Workflow and Component architecture is proposed for solutions based on these technologies and they are compared to identify which is a feasible solution for the use case. Trusted Execution Environments was concluded to be the best match for the requirements of the use case and Secret Network which is a blockchain built on this privacy technology was evaluated against determined privacy metrics and benchmarks were run to check the performance changes due to using the technology. Based on this analysis, Secret Network was found to be a good solution to handle the provided use case and flexible enough to handle more complex requirements. / Kraven på integritet har blivit en nödvändighet i dagens internetbaserade tillämpningar. Detta gäller från traditionella klient-server-tillämpningar till blockkedjebaserade tillämpningar. Eftersom blockkedjor är ett nytt område för utveckling av tillämpningar har man inte prioriterat integritet utöver pseudoanonymitet. I och med att finansiella tillämpningar som byggs på blockkedjor börjar bli allmänt accepterade, och att dessa tillämpningar hanterar känsliga uppgifter om användarna, är det bra att kunna förstå hur integritetsskyddstekniker kan bidra till att se till att användarnas integritet bevaras. Detta projekt tar itu med detta genom att ta ett enkelt användningsfall för finansiella transaktioner och tillämpa olika integritetsskyddstekniker som datakryptering, bevis för nollkunskap och betrodda utförandemiljöer. Arbetsflöden och komponentarkitektur föreslås för lösningar som bygger på dessa tekniker och de jämförs för att identifiera vilken lösning som är genomförbar för användningsfallet. Trusted Execution Environments konstaterades vara den bästa lösningen för kraven i användningsfallet och Secret Network, som är en blockkedja byggd på denna teknik för skydd av privatlivet, utvärderades mot fastställda integritetsmått och benchmarks kördes för att kontrollera prestandaförändringarna till följd av användningen av tekniken. På grundval av denna analys konstaterades Secret Network vara en bra lösning för att hantera det aktuella användningsfallet och tillräckligt flexibel för att hantera mer komplexa krav.

Processen att skapa innehåll till digitala spel för hand är kostsamt och tidskrävande. Allteftersom spelindustrin expanderar ökar behovet av att minska produktionskostnaderna. En lösning på detta problem som det forskas om idag är procedurell generering av spelinnehåll. Kortfattat innebär detta att en algoritm gör det manuella arbetet istället för en designer. I denna uppsats presenterar vi en sådan metod för att automatisera processen att skapa kartor i digitala spel. Vår metod använder kontrollerbara agenter med blandade initiativ (dvs. designern och algoritmen turas om) för att skapa geometri. Vi använder stokastiska agenter för att skapa variation och deterministiska agenter för att garantera spelbarhet. För att kontrollera dessa agenter använder vi en uppsättning parametrar som kan manipuleras. Däröver har designern tillgång till ett antal verktyg inklusive möjligheten att låsa befintlig geometri, konvertera geometri till andra typer, lägga till geometri manuellt, och även möjligheten att använda agenter på specifika områden på kartan. Vi tittar på spelläget Battle i det digitala spelet Mario Kart 64 och visar hur vår metod kan användas för att skapa sådana kartor. Vi utförde en användarstudie på outputen från metoden och resultatet visar att kvaliteten är i allmänhet gynnsam. / The process of creating content for digital games by hand is a costly and time consumingone. As the game industry expands, the need to reduce costs becomes ever more pressing.One solution to this problem being research today is procedural generation of content.In short, this means that an algorithm does the labor rather than a designer. In thisthesis we present such a method for automating the process of creating maps in digitalgames. Our method uses controllable software agents and mixed initiative (i.e. allowingthe designer and algorithm to take turns) to create geometry. We use stochastic agentsto create variation and deterministic agents to ensure playability. To control these agentswe use a set of input parameters which can be manipulated. Furthermore, the designerhas access to a number of tools including the ability to lock existing geometry, convertgeometry to other types, add geometry manually, as well as the ability to use agents onspecific areas of the map. We look at the game mode Battle in the digital game MarioKart 64 and show how our method can be used to create such maps. We conducted auser study on the output of the method and the results show that the quality is generallyfavorable.

[pt] Este trabalho é uma elaboração, com exemplos, e evolução do Algoritmo de Compressão Horizontal (HC) apresentado e seu Conjunto de Regras de Compressão. Este trabalho apresenta uma prova, feita no Provador Interativo de Teoremas Lean, de que o algoritmo HC pode obter uma Derivação Comprimida, representada por um Grafo Acíclico Dirigido, a partir de qualquer Derivação Tipo-Árvore em Dedução Natural para a Lógica Minimal Puramente Implicacional. Finalmente, a partir da Cobertura e Corretude do algoritmo HC, pode-se argumentar que NP = PSPACE. / [en] This work is an elaboration, with examples, and evolution of the presented Horizontal Compression Algorithm (HC) and its set of Compression Rules. This work argues a proof, done in the Lean Interactive Theorem Prover, that the HC algorithm can obtain a Compressed Derivation, represented by a Directed Acyclic Graph, from any Tree-Like Natural Deduction Derivation in Minimal Purely Implicational Logic. Finally, from the Coverage and Soundness of the HC algorithm, one can argue that NP = PSPACE.

Både elever och lärare på gymnasienivå har svårigheter med bevis och bevisföring. Dessutom har det visat sig att bevis och bevisföring spelar en begränsad roll i matematikundervisning. Hur lärare ser på bevisets roll i matematikundervisningen kan påverka tillvägagångssättet för bevisundervisning. Syftet med studien är att belysa hur lärare ser på bevis och bevisföring när det gäller matematikundervisning på gymnasienivå. I studien har nio matematiklärare intervjuats om deras syn på bevisets roll i undervisningen, och hur de arbetar i praktiken med bevis och bevisföring. Intervjudata har analyserats tematiskt, baserat på en teori inspirerad av Knuths (2002a; 2002b) forskning om lärarnas uppfattningar om bevis. Teorin listar sex funktioner som bevis kan ha i matematikundervisning. Det framgår av studien att de flesta lärarna prioriterar förklaring, kommunikation och utveckling av logiskt tänkande när det gäller bevisets roll i undervisning. Resultaten visar även att lärarna anser att bevisundervisning främjar utvecklingen av problemlösningsförmågan. Den strukturerade progressionen och användningen av logiska steg som präglar bevisföringsprocessen utgör grunden för problemlösning. Det kan därför ses som rimligt att införa fler bevisföringsmoment i matematikundervisning. / Both pupils and teachers at upper-secondary school level have difficulties with proof and proving. Furthermore, proof and proving have been shown to play a limited role in mathematics teaching. How teachers view the role of proof in mathematics teaching can affect their approach to teaching proof. The aim of the study was to examine how teachers view proof and proving in the context of mathematics teaching at upper-secondary school level. Nine teachers were interviewed about how they viewed the role of proof in teaching and how they worked in practice with proof and proving. The data was analysed thematically, based on a theory inspired by Knuth’s (2002a; 2002b) research into teachers’ conceptions of proof. The theory lists six functions that proof can have in mathematics teaching. The study shows that most of the teachers prioritise explanation, communication and development of logical thinking as the roles of proof in teaching. The results also show that teachers believe that the teaching of proof promotes the development of problem-solving skills. The proving process is characterized by structured progression and use of logical steps that form the basis for problem-solving. It is therefore reasonable to include more teaching of proof in mathematics education.

Startups within the tech field are incraesingly using proof of concept (POC) customers as a partner when developing new products and services as this enables them to sell the product before building it, ensuring that the product they are developing is aligned with the market needs before making it avaliable to a wider market. Becasue of the positive results that designing and developing new products together with users and customers have shown, the acqusition of POC customers has become a crucial step in the product development process for many startups. The purpose of this study is to understand how the process from business idea to first proof of concept customer evolves and in this process, what are important factors in acquiring the first proof of concept customer. The study is of qualitative nature and leverages a multiple case study based on interviews with eight Swedish tech startups. The findings from the research show that the process is of iterative nature and has seven sub-processes; Defining and scoping proclem, Defining target marker, Finding customers, Defining customer needs, Initial pitch, Persuasion, and finally, Negotiation and signature. Furthermore, five concepts influencing this process were found; Market understanding, Product understanding, Sales tactics, Customer management, and Entrepreneurial attitude. / Startups som verkar inom techindustrin inkluderar allt oftare proof of concept (POC) kunder i utvecklingen av nya produkter och tjänster då det gör det möjligt att säkerställa att produkten är anpassad till marknadens behov. Då utveckling av nya produkter tillsammans med användare och kunder har visat sig effektivt och ha positiva resultat, har förvärvet av POC kunder blivit ett abgörande steg i produktutvecklingsprocessen för många startups. Syftet med denna studie är att förstå hur processen ser ut från affärsidé till signering av första proof of concept kunden, och i denna process även förstå vilka faktorer som är viktiga för att signera första proof of concept-kunden. Studien är av kvalitativ karaktär och använder fallstudier baserad på intervjuer med åtta svenska tech startups. Resultaten visar att processen är av iterativ natur och har sju delprocesser; Definiera problemet, Definiera målgrupp, Hitta kunder, Definiera kundbehov, Inledande pitch, Övertalning och slutligen, Förhandling och signatur. Vidare presenteras fem koncept som påverkar denna proccess; Marknadsförståelse, Produktförståelse, Säljtaktik, Kundhantering och Entreprenöriell attityd.

Eine Herausforderung der Softwareentwicklung ist, die Korrektheit einer Software sicherzustellen. Testen bietet es keine mathematische Korrektheit. Formale Verifikation ist jedoch oft zu aufwändig. Laufzeitverifikation steht zwischen den beiden Methoden. Laufzeitverifikation beantwortet die Frage, ob ein Eingabe-Ausgabe-Paar korrekt ist. Ein zertifizierender Algorithmus überzeugt seinen Nutzer durch ein Korrektheitsargument zur Laufzeit. Dafür berechnet ein zertifizierender Algorithmus für eine Eingabe zusätzlich zur Ausgabe noch einen Zeugen – ein Korrektheitsargument. Jeder zertifizierende Algorithmus besitzt ein Zeugenprädikat: Ist dieses erfüllt für eine Eingabe, eine Ausgabe und einen Zeugen, so ist das Eingabe-Ausgabe-Paar korrekt. Ein simpler Algorithmus, der das Zeugenprädikat für den Nutzer entscheidet, ist ein Checker. Die Korrektheit des Checkers ist folglich notwendig für den Ansatz und die formale Instanzverifikation, bei der wir Checker verifizieren und einen maschinen-geprüften Beweis für die Korrektheit eines Eingabe-Ausgabe-Paars zur Laufzeit gewinnen. Zertifizierende sequentielle Algorithmen sind gut untersucht. Verteilte Algorithmen, die auf verteilten Systemen laufen, unterscheiden sich grundlegend von sequentiellen Algorithmen: die Ausgabe ist über das System verteilt oder der Algorithmus läuft fortwährend. Wir untersuchen zertifizierende verteilte Algorithmen. Unsere Forschungsfrage ist: Wie können wir das Konzept zertifizierender sequentieller Algorithmen so auf verteilte Algorithmen übertragen, dass wir einerseits nah am ursprünglichen Konzept bleiben und andererseits die Gegebenheiten verteilter Systeme berücksichtigen? Wir stellen eine Methode der Übertragung vor. Die beiden Ziele abwägend entwickeln wir eine Klasse zertifizierender verteilter Algorithmen, die verteilte Zeugen berechnen und verteilte Checker besitzen. Wir präsentieren Fallstudien, Entwurfsmuster und ein Framework zur formalen Instanzverifikation. / A major problem in software engineering is to ensure the correctness of software. Testing offers no mathematical correctness. Formal verification is often too costly. Runtime verification stands between the two methods. Runtime verification answers the question whether an input-output pair is correct. A certifying algorithm convinces its user at runtime by offering a correctness argument. For each input, a certifying algorithm computes an output and additionally a witness. Each certifying algorithm has a witness predicate – a predicate with the property: being satisfied for an input, output and witness implies the input-output pair is correct. A simple algorithm deciding the witness predicate for the user is a checker. Hence, the checker’s correctness is crucial to the approach and motivates formal instance verification where we verify checkers and obtain machine-checked proofs for the correctness of an input-output pair at runtime. Certifying sequential algorithms are well-established. Distributed algorithms, designed to run on distributed systems, behave fundamentally different from sequential algorithms: their output is distributed over the system or they even run continuously. We investigate certifying distributed algorithms. Our research question is: How can we transfer the concept of certifying sequential algorithms to distributed algorithms such that we are in line with the original concept but also adapt to the conditions of distributed systems? In this thesis, we present a method to transfer the concept: Weighing up both sometimes conflicting goals, we develop a class of certifying distributed algorithms that compute distributed witnesses and have distributed checkers. We offer case studies, design patterns and a framework for formal instance verification. Additionally, we investigate other methods to transfer the concept of certifying algorithms to distributed algorithms.

Die Theorie disjunkter NP-Paare, die auf natürliche Weise statt einzelner Sprachen Paare von NP-Mengen zum Objekt ihres Studiums macht, ist vor allem wegen ihrer Anwendungen in der Kryptografie und Beweistheorie interessant. Im Zentrum dieser Dissertation steht die Analyse der Beziehung zwischen disjunkten NP-Paaren und aussagenlogischen Beweissystemen. Haben die Anwendungen der NP-Paare in der Beweistheorie maßgeblich das Verständnis aussagenlogischer Beweissysteme gefördert, so beschreiten wir in dieser Arbeit gewissermaßen den umgekehrten Weg, indem wir Methoden der Beweistheorie zur genaueren Untersuchung des Verbands disjunkter NP-Paare heranziehen. Insbesondere ordnen wir jedem Beweissystem P eine Klasse DNPP(P) von NP-Paaren zu, deren Disjunktheit in dem Beweissystem P mit polynomiell langen Beweisen gezeigt werden kann. Zu diesen Klassen DNPP(P) zeigen wir eine Reihe von Resultaten, die illustrieren, dass robust definierten Beweissystemen sinnvolle Komplexitätsklassen DNPP(P) entsprechen. Als wichtiges Hilfsmittel zur Untersuchung aussagenlogischer Beweissysteme und der daraus abgeleiteten Klassen von NP-Paaren benutzen wir die Korrespondenz starker Beweissysteme zu erststufigen arithmetischen Theorien, die gemeinhin unter dem Schlagwort beschränkte Arithmetik zusammengefasst werden. In der Praxis trifft man statt auf zwei häufig auf eine größere Zahl konkurrierender Bedingungen. Daher widmen wir uns der Erweiterung der Theorie disjunkter NP-Paare auf disjunkte Tupel von NP-Mengen. Unser Hauptergebnis in diesem Bereich besteht in der Charakterisierung der Fragen nach der Existenz optimaler Beweissysteme und vollständiger NP-Paare mit Hilfe disjunkter Tupel. / Disjoint NP-pairs are an interesting complexity theoretic concept with important applications in cryptography and propositional proof complexity. In this dissertation we explore the connection between disjoint NP-pairs and propositional proof complexity. This connection is fruitful for both fields. Various disjoint NP-pairs have been associated with propositional proof systems which characterize important properties of these systems, yielding applications to areas such as automated theorem proving. Further, conditional and unconditional lower bounds for the separation of disjoint NP-pairs can be translated to results on lower bounds to the length of propositional proofs. In this way disjoint NP-pairs have substantially contributed to the understanding of propositional proof systems. Conversely, this dissertation aims to transfer proof-theoretic knowledge to the theory of NP-pairs to gain a more detailed understanding of the structure of the class of disjoint NP-pairs and in particular of the NP-pairs defined from propositional proof systems. For a proof system P we introduce the complexity class DNPP(P) of all disjoint NP-pairs for which the disjointness of the pair is efficiently provable in the proof system P. We exhibit structural properties of proof systems which make the previously defined canonical NP-pairs of these proof systems hard or complete for DNPP(P). Moreover, we demonstrate that non-equivalent proof systems can have equivalent canonical pairs and that depending on the properties of the proof systems different scenarios for DNPP(P) and the reductions between the canonical pairs exist. As an important tool for our investigation we use the connection of propositional proof systems and disjoint NP-pairs to theories of bounded arithmetic.