[pt] O tamanho das provas formais possui algumas importantes implicações teóricas na área da complexidade computacional. O problema de determinar se uma fórmula é uma tautologia da Lógica Proposicional Intuicionista e do fragmento puramente implicacional da Lógica Minimal (M(contém)) é PSPACE- Completo. Qualquer lógica proposicional com um sistema de dedução natural que satisfaça o princípio da subfórmula possui o problema de determinar tautologias em PSPACE. Saber se qualquer tautologia em M(contém) admite provas de tamanho polinomialmente limitado está relacionado com saber se NP = PSPACE. Técnicas de compressão de provas reportadas na literatura utilizam duas abordagens principais para comprimir provas: gerar provas já compactadas; comprimir uma prova já gerada. Proposta por Gordeev e Haeusler (6), a Compressão Horizontal é uma técnica de compressão de provas em dedução natural da M(contém) que utiliza grafos direcionados para representar as provas. Dada a prova de uma tautologia qualquer da M(contém), que pode possuir tamanho exponencial em relação ao tamanho da conclusão, o objetivo da Compressão Horizontal é que a prova resultante da compressão possua tamanho polinomialmente limitado em relação ao tamanho da conclusão. Nosso trabalho apresenta a primeira implementação da Compressão Horizontal, juntamente com os primeiros resultados da aplicação da técnica sobre provas de tautologias da M(contém), além disso, compara as taxas de compressão obtidas com técnicas tradicionais de compressão de dados. / [en] The size of formal proofs has some important theoretical implications in computational complexity theory. The problem of determining if some formula of Intuitionistic Propositional Logic and the purely implicational fragment of Minimal Logic (M(contains)) is a tautology is PSPACE-Complete. Any propositional logic with a natural deduction system that satisfies the sub- formula principle is PSPACE. To know if any tautology in M(contains) admits polynomially sized proof is related to whether NP = PSPACE. Proof compression techniques reported in literature use two main approaches to proof compressing: generating already compressed proofs; compressing an already generated proof. Proposed by Gordeev and Haeusler (6), the Horizontal Compression is a natural deduction proof compression technique that uses directed graphs to represent proofs. Given a tautology proof in M(contains), which may have an exponential size in relation to conclusion length, the goal of Horizontal Compression is that the compressed proof has a polynomially limited size in relation to conclusion length. Our work presents the first implementation of Horizontal Compression, together with the first results of the execution of the technique on proofs of M(contains) tautologies.

L'apprentissage des preuves mathématiques déductives est fondamental dans l'enseignement des mathématiques. Pourtant, la dernière enquête TIMSS (Trends in International Mathematics and Science Study) menée par l'IEA ("International Association for the Evaluation of Educational Achievement") en mars 2015, le niveau général des étudiants en mathématiques est en baisse et les étudiants éprouvent de plus en plus de difficultés pour comprendre et écrire les preuves mathématiques déductives.Pour aborder ce problème, plusieurs travaux en didactique des mathématiques utilisent l’apprentissage collaboratif en classe.L'apprentissage collaboratif consiste à regrouper des étudiants pour travailler ensemble dans le but d'atteindre un objectif commun. Il repose sur le débat et l'argumentation. Les étudiants s'engagent dans des discussions pour exprimer leurs points de vue sous forme d'arguments et de contre-arguments dans le but de résoudre un problème posé.L’argumentation utilisée dans ces approches est basée sur des discussions informelles qui permettent aux étudiants d'exprimer publiquement leurs déclarations et de les justifier pour construire des preuves déductives. Ces travaux ont montré que l’argumentation est une méthode efficace pour l’apprentissage des preuves mathématiques : (i) elle améliore la pensée critique et les compétences métacognitives telles que l'auto-surveillance et l'auto-évaluation (ii) augmente la motivation des étudiants par les interactions sociales et (iii) favorise l'apprentissage entre les étudiants. Du point de vuedes enseignants, certaines difficultés surgissent avec ces approches pour l'évaluation des preuves déductives. En particulier, l'évaluation des résultats, qui comprend non seulement la preuve finale mais aussi les étapes intermédiaires, les discussions, les conflits qui peuvent exister entre les étudiants durant le débat. En effet, cette évaluation introduit une charge de travail importante pour les enseignants.Dans cette thèse, nous proposons un système pour la construction et l'évaluation des preuves mathématiques déductives. Ce système a un double objectif : (i) permettre aux étudiants de construire des preuves mathématiques déductives à partir un débat argumentatif structuré (ii) aider les enseignants à évaluer ces preuves et toutes les étapes intermédiaires afin d'identifier les erreurs et les lacunes et de fournir un retour constructif aux étudiants.Le système offre aux étudiants un cadre structuré pour débattre durant la construction de la preuve en utilisant les cadres d'argumentation proposés en intelligente artificielle. Ces cadres d’argumentation sont utilisés aussi dans l’analyse du débat qui servira pour représenter le résultat sous différentes formes afin de faciliter l’évaluation aux enseignants. Dans un second temps, nous avons implanté et validé le système par une étude expérimentale pour évaluer son acceptabilité dans la construction collaborative des preuves déductives par les étudiants et dans l’évaluation de ces preuves par les enseignants. / Learning deductive proofs is fundamental for mathematics education. Yet, many students have difficulties to understand and write deductive mathematical proofs which has severe consequences for problem solving as highlighted by several studies. According to the recent study of TIMSS (Trends in International Mathematics and Science Study), the level of students in mathematics is falling. students have difficulties to understand mathematics and more precisely to build and structure mathematical proofs.To tackle this problem, several approaches in mathematical didactics have used a social approach in classrooms where students are engaged in a debate and use argumentation in order to build proofs.The term "argumentation" in this context refers to the use of informal discussions in classrooms to allow students to publicly express claims and justify them to build proofs for a given problem. The underlying hypotheses are that argumentation: (i) enhances critical thinking and meta-cognitive skills such as self monitoring and self assessment; (ii) increases student's motivation by social interactions; and (iii) allows learning among students. From instructors' point of view, some difficulties arise with these approaches for assessment. In fact, the evaluation of outcomes -- that includes not only the final proof but also all intermediary steps and aborted attempts -- introduces an important work overhead.In this thesis, we propose a system for constructing and evaluating deductive mathematical proofs. The system has a twofold objective: (i) allow students to build deductive mathematical proofs using structured argumentative debate; (ii) help the instructors to evaluate these proofs and assess all intermediary steps in order to identify misconceptions and provide a constructive feedback to students. The system provides students with a structured framework to debate during construction of proofs using the proposed argumentation frameworks in artificial intelligence. These argumentation frameworks are also used in the analysis of the debate which will be used to represent the result in different forms in order to facilitate the evaluation to the instructors. The system has been implemented and evaluated experimentally by students in the construction of deductive proofs and instructors in the evaluation of these proofs.

Esta tese aborda a distribuição do ônus da prova no processo trabalhista pretendendo a aplicação da teoria da distribuição dinâmica do onus probandi neste ramo processual especial. Na primeira parte do trabalho são examinadas questões relativas aos direitos fundamentais, bem assim aos princípios constitucionais processuais, com relevo especial ao direito constitucional à prova. Na sequência serão estudadas as matérias relativas ao ônus da prova na teoria geral do processo, suas dimensões, os poderes instrutórios do juiz, a teoria clássica da distribuição do ônus da prova, bem assim as especificidades da inversão da prova no processo do trabalho. Segue-se a abordagem com a apresentação de teoria dinâmica do ônus da prova e sua recepção pelo direito brasileiro, apontando ainda alguns projetos legislativos que já positivam sua adoção no Brasil. Por fim, e considerando a necessidade de superação das regras estáticas do ônus da prova no direito processual do trabalho propõe-se a adoção das regras dinâmicas, partindo da necessidade de efetividade da tutela jurisdicional e concretização dos princípios da igualdade substancial, tudo em observância ao direito fundamental a um processo do trabalho justo e igualitário. Serão, ainda, abordadas algumas decisões jurisprudenciais da Justiça do Trabalho que aplicam o ônus dinâmico da prova. / The present thesis addresses the distribution of the burden of proof in labor procedural law aiming to apply the theory of dynamic distribution of the onus probandi in this branch of special procedural law. In the first part of this paper, issues related to the fundamental rights, as well as procedural constitutional principles, will be assessed, with special emphasis to the constitutional right to poof. Subsequently, matters related to the burden of proof in general procedural theory, its dimensions, the instruction powers of the judge, the classic theory of distribution of the burden of proof, as well as the specificities of the inversion of the proof burden in labor procedural law will be analyzed. Then, an approach to the dynamic theory of the burden of proof and its reception in Brazilian law is presented, highlighting some legislative projects that already indicate the positive adoption in Brazil. Finally, and considering the urge to overcome the static rules of the proof burden in labor procedural law, we propose the adoption of the dynamic rules, from the standpoint of the need for effectiveness in jurisdictional custody and materialization of the principles of substantial equality, in observance of the fundamental right to a fair and equalitarian labor proceeding. And yet, some case law rulings of the Labor Justice applying the principle of dynamic burden of proof will be addressed.

Esta tese aborda a distribuição do ônus da prova no processo trabalhista pretendendo a aplicação da teoria da distribuição dinâmica do onus probandi neste ramo processual especial. Na primeira parte do trabalho são examinadas questões relativas aos direitos fundamentais, bem assim aos princípios constitucionais processuais, com relevo especial ao direito constitucional à prova. Na sequência serão estudadas as matérias relativas ao ônus da prova na teoria geral do processo, suas dimensões, os poderes instrutórios do juiz, a teoria clássica da distribuição do ônus da prova, bem assim as especificidades da inversão da prova no processo do trabalho. Segue-se a abordagem com a apresentação de teoria dinâmica do ônus da prova e sua recepção pelo direito brasileiro, apontando ainda alguns projetos legislativos que já positivam sua adoção no Brasil. Por fim, e considerando a necessidade de superação das regras estáticas do ônus da prova no direito processual do trabalho propõe-se a adoção das regras dinâmicas, partindo da necessidade de efetividade da tutela jurisdicional e concretização dos princípios da igualdade substancial, tudo em observância ao direito fundamental a um processo do trabalho justo e igualitário. Serão, ainda, abordadas algumas decisões jurisprudenciais da Justiça do Trabalho que aplicam o ônus dinâmico da prova. / The present thesis addresses the distribution of the burden of proof in labor procedural law aiming to apply the theory of dynamic distribution of the onus probandi in this branch of special procedural law. In the first part of this paper, issues related to the fundamental rights, as well as procedural constitutional principles, will be assessed, with special emphasis to the constitutional right to poof. Subsequently, matters related to the burden of proof in general procedural theory, its dimensions, the instruction powers of the judge, the classic theory of distribution of the burden of proof, as well as the specificities of the inversion of the proof burden in labor procedural law will be analyzed. Then, an approach to the dynamic theory of the burden of proof and its reception in Brazilian law is presented, highlighting some legislative projects that already indicate the positive adoption in Brazil. Finally, and considering the urge to overcome the static rules of the proof burden in labor procedural law, we propose the adoption of the dynamic rules, from the standpoint of the need for effectiveness in jurisdictional custody and materialization of the principles of substantial equality, in observance of the fundamental right to a fair and equalitarian labor proceeding. And yet, some case law rulings of the Labor Justice applying the principle of dynamic burden of proof will be addressed.

The introduction of Physical Unclonable Functions (PUFs) and lightweight consensus algorithms to aid in the bolstering of security and privacy in both IoT and IoE does show a great deal of promise not only in these areas, but in resource cost over traditional methods of blockchain.  However, several previous studies make claims regarding performance of novel solutions without providing detailed information as to the physical components of their experiments.  This comparative study shows that Proof of Authentication (PoAh) performs the best out of three selected consensus algorithms and that the claims made regarding the performance of PUFChain and Proof of PUF-enabled Authentication (PoP) could not be replicated in this instance.

Název práce: O síle slabých rozšírení teorie V0 Autor: Sebastian Müller Katedra: Katedra Algebry Vedoucí disertační práce: Prof. RNDr. Jan Krajíček, DrSc., Katedra Algebry. Abstrakt: V predložené disertacní práci zkoumáme sílu slabých fragmentu arit- metiky. Činíme tak jak z modelově-teoretického pohledu, tak z pohledu důkazové složitosti. Pohled skrze teorii modelu naznačuje, že malý iniciální segment libo- volného modelu omezené aritmetiky bude modelem silnější teorie. Jako příklad ukážeme, že každý polylogaritmický řez modelu V0 je modelem VNC. Užitím známé souvislosti mezi fragmenty omezené aritmetiky a dokazatelností v ro- zličných důkazových systémech dokážeme separaci mezi rezolucí a TC0 -Frege systémem na náhodných 3CNF-formulích s jistým poměrem počtu klauzulí vůci počtu proměnných. Zkombinováním obou výsledků dostaneme slabší separační výsledek pro rezoluci a Fregeho důkazové systémy omezené hloubky. Klíčová slova: omezená aritmetika, důkazová složitost, Fregeho důkazový systém, Fregeho důkazový systém omezené hloubky, rezoluce Title: On the Power of Weak Extensions of V0 Author: Sebastian Müller Department: Department of Algebra Supervisor: Prof. RNDr. Jan Krajíček, DrSc., Department of Algebra....

No description available.

The discovery of unknown lemmas, case-splits and other so called eureka steps are challenging problems for automated theorem proving and have generally been assumed to require user intervention. This thesis is mainly concerned with the automated discovery of inductive lemmas. We have explored two approaches based on failure recovery and theory formation, with the aim of improving automation of firstand higher-order inductive proofs in the IsaPlanner system. We have implemented a lemma speculation critic which attempts to find a missing lemma using information from a failed proof-attempt. However, we found few proofs for which this critic was applicable and successful. We have also developed a program for inductive theory formation, which we call IsaCoSy. IsaCoSy was evaluated on different inductive theories about natural numbers, lists and binary trees, and found to successfully produce many relevant theorems and lemmas. Using a background theory produced by IsaCoSy, it was possible for IsaPlanner to automatically prove more new theorems than with lemma speculation. In addition to the lemma discovery techniques, we also implemented an automated technique for case-analysis. This allows IsaPlanner to deal with proofs involving conditionals, expressed as if- or case-statements.

<p>Development of colour management systems, the level ofstandardisation, as well as the embedding of facilities forcolour management into computer operating systems and software,enables successful future interoperability of colour reproductionin the graphic arts industry. Yet colour reproduction from onemedium to another, still gives rise to inconsistencies.</p><p>This thesis investigates colour management and controlprocesses in premedia and press process workflows in graphic artsproduction, including standards, instruments and procedures. Thegoal is to find methods for higher efficiency and control ofcolour print media production processes, aiming at increasingcolour consistency and process automation and of reducingoverheads. The focus is on the control of colour data by displaysin prepress processes producing low quality paper products. Inthis respect the greatest interest of this thesis is on technicaland visual characteristics of displays with respect tp thereproduction of colour, especially desktop Thin Film TransistorLiquid Crystal Displays (TFTLCD) compared to portable TFTLCDs andCathod Ray Tube (CRT) monitors.</p><p>In order to reach the desired goal, this thesis is based on aliterature survey and empirical studies. The empirical studiesinclude both qualitative and quantitative methods, organised intothree parts:</p><p>    Colour process management: Analysed case studies of theimplementation of colour management in entire graphic artsproduction workflow processes.</p><p>    Display technology: LCD and CRT displays have been examinedthrough measurements to establish their fundamental strengthsand weaknesses in reproducing colours.</p><p>    Comparison of reproduction: A perceptual experiment hasbeen conducted to determine the ability of the disparatecomponents included in a colour management system to co-operateand match reproduced colour, according to the perceivedpreference of observers.</p><p>It was found that in most cases consistent colour fidelitydepends on the knowledge and experience of the actors involved inthe production process, including the utilisation of routines andequipment. Lack of these factors is not necessarily fatal for thefinal low quality paper colour product, but obstructs theautomation. In addition, increased digitalisation will increasethe importance of displays in such processes. The results showthat CRTs and desktop LCDs meet most of the demands of colourreproduction in various areas of low quality paper productionprocesses, e.g. newspaper production. However, some fundamentalaspects, such as low digital input values, viewing angles andcolour temperature, matters that concern characterisation andcalibration, still need to be developed. Concerning softproofing, the matching correspondence between hard and softcopies gives similar results for both CRT and LCDs forhigh-quality paper originals, if the luminance is decreased onthe LCD (to luminance levels of CRTs). Soft proofing of lowquality papers gives equally lower matching agreement for bothCRT and LCD, in this case when the luminance of the LCD is sethigher (e.g. about twice the levels luminance levels ofCRTs).</p><p><b>Keywords:</b>Displays, LCD, CRT, premedia, prepress, softproof, workflows, newspaper, colour management systems, colourcontrol, colour reproduction</p>

<p>This thesis aims to describe how students encounter proof in a community of mathematical practice at a mathematics department and how they are drawn to share mathematicians’ views and knowledge of proof. Considering the department as a <i>community of practice </i>where the joint enterprise is learning mathematics in a broad sense made it possible to perceive the newcomers as active participants in the practice. The combination of a socio-cultural perspective, Lave and Wenger’s and Wenger’s social practice theories and theories about proof offers a fresh framework in understanding and describing the diversity of the culture involving such a complex notion as proof. Proof is examined from historical, philosophical and didactical points of view and considered as <i>reification </i>and as an <i>artefact </i>from a socio-cultural perspective. The metaphor of <i>transparency</i> of artefacts that refers to the intricate dilemma about how much to focus on different aspects of proof at a meta-level and how much to work with proof without focusing on it, both from teacher and student perspectives, is a fundamental aspect in the data analysis. The data consists of transcripts of interviews with mathematicians and students as well as survey responses of university entrants, protocols of observations of lectures, textbooks and other instructional material. Both qualitative and quantitative methods were applied in the data analysis. A theoretical model with three different teaching styles with respect to proof could be constructed from the data. The students related positively to proof when they entered the practice. Though the mathematicians had no explicit intention of dealing so much with proof in the basic course, students felt that they were confronted with proof from the very beginning of their studies. Proof was there as a mysterious artefact and a lot of aspects of proof remained invisible as experienced by students when they struggled to find out what proof is and to understand its role and meaning in the practice. The first oral examination in proof seems to be significant in drawing students to the practice of proof.</p>