Whilst results from Structural Proof Theory can be couched in many formalisms, it is the sequent calculus which is the most amenable of the formalisms to metamathematical treatment. Constructive syntactic proofs are filled with bureaucratic details; rarely are all cases of a proof completed in the literature. Two intermediate results can be used to drastically reduce the amount of effort needed in proofs of Cut admissibility: Weakening and Invertibility. Indeed, whereas there are proofs of Cut admissibility which do not use Invertibility, Weakening is almost always necessary. Use of these results simply shifts the bureaucracy, however; Weakening and Invertibility, whilst more easy to prove, are still not trivial. We give a framework under which sequent calculi can be codified and analysed, which then allows us to prove various results: for a calculus to admit Weakening and for a rule to be invertible in a calculus. For the latter, even though many calculi are investigated, the general condition is simple and easily verified. The results have been applied to G3ip, G3cp, G3s, G3-LC and G4ip. Invertibility is important in another respect; that of proof-search. Should all rules in a calculus be invertible, then terminating root-first proof search gives a decision procedure for formulae without the need for back-tracking. To this end, we present some results about the manipulation of rule sets. It is shown that the transformations do not affect the expressiveness of the calculus, yet may render more rules invertible. These results can guide the design of efficient calculi. When using interactive proof assistants, every case of a proof, however complex, must be addressed and proved before one can declare the result formalised. To do this in a human readable way adds a further layer of complexity; most proof assistants give output which is only legible to a skilled user of that proof assistant. We give human-readable formalisations of Cut admissibility for G3cp and G3ip, Contraction admissibility for G4ip and Craig's Interpolation Theorem for G3i using the Isar vernacular of Isabelle. We also formalise the new invertibility results, in part using the package for reasoning about first-order languages, Nominal Isabelle. Examples are given showing the effectiveness of the formalisation. The formal proof of invertibility using the new methods is drastically shorter than the traditional, direct method.

The case for interfacing logic tools together has been made countless times in the literature, but it is still an important research question. There are various logics and respective tools for carrying out formal developments, but practitioners still lament the difficulty of reliably exchanging mathematical data between tools. Writing proof-translation tools is hard. The problem has both a theoretical side (to ensure that the translation is adequate) and a practical side (to ensure that the translation is feasible and usable). Moreover, the source and target proof formats might be less documented than desired (or even necessary), and this adds a dash of reverse-engineering to what should be a system integration task. This dissertation studies proof translation for higher-order logic. We will look at the qualitative benefits of locating the translation close to the source (where the proof is generated), the target (where the proof is consumed), and in between (as an independent tool from the proof producer and consumer). Two ideas are proposed to alleviate the difficulty of building proof translation tools. The first is a proof translation framework that is structured as a compiler. Its target is specified as an abstract machine, which captures the essential features of its implementations. This framework is designed to be performant and extensible. Second, we study proof transformations that convert refutation proofs from a broad class of consistency-preserving calculi (such as those used by many proof-finding tools) into proofs in validity-preserving calculi (the kind used by many proof-checking tools). The basic method is very simple, and involves applying a single transformation uniformly to all of the source calculi's inferences, rather than applying ad hoc (rule specific) inference interpretations.

The emphasis of undergraduate mathematics content is centered around abstract reasoning and proof, whereas students' pre-college mathematical experiences typically give them limited exposure to these concepts. Not surprisingly, many students struggle to make the transition to undergraduate mathematics in their first course on mathematical proof, known as a bridge course. In the process of this study, eight students of varied backgrounds were interviewed before during and after their bridge course at BYU. By combining the proof scheme frameworks of Harel and Sowder (1998) and Ko and Knuth (2009), I analyzed and categorized students’ initial proof schemes, observed their development throughout the semester, and their proof schemes upon completing the bridge course. It was found that the proof schemes used by the students improved only in avoiding empirical proofs after the initial interviews. Several instances of ritual proof schemes used to generate adequate proofs were found, calling into question the goals of the bridge course. Additionally, it was found that students’ proof understanding, production, and appreciation may not necessarily coincide with one another, calling into question this hypothesis from Harel and Sowder (1998).

No description available.

Proof planning is a paradigm for the automation of proof that focuses on encoding intelligence to guide the proof process. The idea is to capture common patterns of reasoning which can be used to derive abstract descriptions of proofs known as proof plans. These can then be executed to provide fully formal proofs. This thesis concerns the development and analysis of a novel approach to proof planning that focuses on an explicit representation of choices during search. We embody our approach as a proof planner for the generic proof assistant Isabelle and use the Isar language, which is human-readable and machine-checkable, to represent proof plans. Within this framework we develop an inductive theorem prover as a case study of our approach to proof planning. Our prover uses the difference reduction heuristic known as rippling to automate the step cases of the inductive proofs. The development of a flexible approach to rippling that supports its various modifications and extensions is the second major focus of this thesis. Here, our inductive theorem prover provides a context in which to evaluate rippling experimentally. This work results in an efficient and powerful inductive theorem prover for Isabelle as well as proposals for further improving the efficiency of rippling. We also draw observations in order to direct further work on proof planning. Overall, we aim to make it easier for mathematical techniques, and those specific to mechanical theorem proving, to be encoded and applied to problems.

Coinduction is a proof rule which is the dual of induction. It allows reasoning about non-well-founded sets and is of particular use for reasoning about equivalences. In this thesis I present an automation of coinductive theorem proving. This automation is based on the ideas of proof planning [Bundy 88]. Proof planning as the name suggests, plans the higher level steps in a proof without performing the formal checking which is also required for a verification. The automation has focused on the use of coinduction to prove the equivalence of programs in a small lazy functional language which is similar to Haskell. One of the hardest parts in a coinductive proof is the choice of a relation, called a bisimulation. The automation here described makes an initial simplified guess at a bisimulation and then uses critics, revisions based on failure, and generalisation techniques to refine this guess. The proof plan for coinduction and the critic have been implemented in CLAM [Bundy et al 90b] with encouraging results. The planner has been successfully tested on a number of theorems. Comparison of the proof planner for coinduction with the proof plan for induction implemented in CLAM has gighlighted a number of equivalences and dualities in the process of these proofs and has also suggested improvements to both systems. This work has demonstrated not only the possibility of fully automated theorem provers for coinduction but has also demonstrated the uses of proof planning for comparison of proof techniques. This work has demonstrated not only the possibility of fully automated theorem provers for coinduction but has also demonstrated the uses of proof planning for comparison of proof techniques.

A key problem in automating proof by mathematical induction is choosing an induction rule suitable for a given conjecture. Since Boyer & Moore’s NQTHM system the standard approach has been based on recursion analysis, which uses a combination of induction rules based on the relevant recursive function definitions. However, there are practical examples on which such techniques are known to fail. Recent research has tried to improve automation by delaying the choice of inductive rule until later in the proof, but these techniques suffer from two serious problems. Firstly, a lack of search control: specifically, in controlling the application of ‘speculative’ proof steps that partially commit to a choice of induction rule. Secondly, a lack of generality: they place significant restrictions on the form of induction rule that can be chosen. In this thesis we describe a new delayed commitment strategy for inductive proof that addresses these problems. The strategy dynamically creates an appropriate induction rule by proving schematic proof goals, where unknown rule structure is represented by meta-variables which become instantiated during the proof. This is accompanied by a proof that the generated rule is valid. The strategy achieves improved control over speculative proof steps via a novel speculation critic. It also generates a wider range of useful induction rules than other delayed commitment techniques, partly because it removes unnecessary restrictions on the individual proof cases, and partly because of a new technique for generating the rule’s overall case structure. The basic version of the strategy has been implemented using the lamdaClam proof planner. The system was extended with a novel proof critics architecture for this purpose. An evaluation shows the strategy is a useful and practical technique, and demonstrates its advantages.

We introduce subatomic logic, a new methodology where by looking inside of atoms we are able to represent a wide variety of proof systems in such a way that every rule is an instance of a single, regular, linear rule scheme. We show the generality of the subatomic approach by presenting how it can be applied to several different systems with very different expressivity. In this thesis we use subatomic logic to study two normalisation procedures: cut-elimination and decomposition. In particular, we study cut-elimination by characterising a whole class of substructural logics and giving a generalised cut-elimination procedure for them, and we study decomposition by providing generalised rewriting rules for derivations that we can then apply to decompose derivations and to eliminate cycles.

O presente trabalho estuda a aplicação da teoria da distribuição dinâmica do ônus da prova no Direito Processual do Trabalho. Analisa, inicialmente, os impactos das novas demandas trabalhistas e das modernas teorias do Direito Processual no Direito Processual do Trabalho. Aborda o ônus da prova em seus aspectos gerais, definindo conceito de prova, conceitos e distinções entre ônus, obrigação e dever e conceito de ônus da prova, analisando a evolução teórica e o perfil dogmático da distribuição do ônus da prova, a estrutura funcional do ônus da prova (ônus da prova subjetivo e ônus da prova objetivo), o ônus da prova de fato negativo, a prova diabólica, a inversão judicial do ônus da prova (com ênfase para a regra prevista no Código de Defesa do Consumidor e o momento processual adequado para tanto) e a relação entre presunções, responsabilidade civil objetiva e o ônus da prova. Estuda aspectos gerais acerca do ônus da prova no Direito Processual do Trabalho, referentes à regra do artigo 818 da Consolidação das Leis do Trabalho, e a aplicação subsidiária do artigo 333 do Código de Processo Civil, e à inversão judicial do ônus da prova no processo juslaboral, com base na aplicação do Código de Defesa do Consumidor, do princípio protetor, do princípio da pré-constituição da prova e do princípio da aptidão para a prova. Analisa aspectos gerais referentes à teoria da distribuição dinâmica do ônus da prova, estabelecendo conceitos e distinções entre distribuição estática, inversão judicial e distribuição dinâmica do ônus da prova, abordando origens históricas e incorporação da teoria no Direito Comparado, fundamentos para aplicação da dinamização da carga probatória no Direito Processual Brasileiro (com ênfase ao direito fundamental à prova, ao princípio da igualdade material no processo, exercício dos poderes instrutórios do juiz, busca da verdade real e regra do artigo 333, parágrafo único, inciso II, do Código de Processo Civil) e incorporação legislativa da teoria no Direito Processual Brasileiro, prevista no Anteprojeto de Código Brasileiro de Processos Coletivos, Projeto de Lei da Ação Civil Pública e Projeto de Código de Processo Civil. Por fim, estuda especificamente a aplicação da teoria da distribuição dinâmica do ônus da prova no Direito Processual do Trabalho, partindo dos fundamentos para sua incidência no processo juslaboral (direito fundamental à prova, princípio da igualdade material no processo e a regra do artigo 852 - D da Consolidação das Leis do Trabalho), abordando critérios objetivos para a aplicação (subsidiariedade, utilização dos poderes instrutórios e das máximas de experiência do juiz, vedação do incentivo ao comodismo processual e à instauração da probatio diabólica reversa, com observância do binômio impossibilidade/extrema dificuldade do empregado na produção da prova-possibilidade/maior facilidade na produção para o empregador, fundamentação da decisão, vedação da carga processual superveniente), momento processual adequado para a dinamização, relação entre nulidades processuais e distribuição dinâmica, instrumento processual cabível para impugnação da incidência da teoria, definição da regra de distribuição do ônus da prova pelos Tribunais e casuísticas de aplicação da distribuição dinâmica do ônus da prova, com exame crítica da doutrina e da jurisprudência, no Direito Processual Individual do Trabalho (abordando os seguintes temas: jornada de trabalho, vale-transporte, equiparação salarial, depósitos do fundo de Garantia do Tempo de Serviço (FGTS), despedimento, salário-família, acidente do trabalho, assédio moral e assédio sexual, discriminação das relações de trabalho, privacidade e intimidade do trabalhador, responsabilidade subsidiária da Administração Pública, grupo econômico, sucessão trabalhista, bem de família e gratuidade processual) e no Direito Processual Coletivo do Trabalho, com formulação de proposta legislativa ao final do estudo. / This work studies the application of the theory of dynamic distribution of the burden of proof on Labor Procedural Law. It examines, initially, the impact of new labor demands and modern theories of the Procedural Law on Labor Procedural Law. It boards the burden of proof in its general aspects, defining concept of proof, concepts and distinctions between burden, obligation and duty and concept of burden of proof, analyzing the theoretical evolution and dogmatic profile of the distribution of the burden of proof, the functional structure of the burden of proof (subjective burden of proof and objective burden of proof), the burden of proof in fact negative, diabolical proof, the judicial reverse of the burden of proof (with emphasis on the rule laid down in the Consumer Defense Code and the appropriate procedural moment for this) and the relation between presumptions, strict liability and burden of proof. It studies general aspects about the burden of proof on Labor Procedural Law, referring to the rule of Artic le 818 of the Consolidation of Labor Laws, and the subsidiary application of Article 333 of the Code of Civil Procedure, and the judicial reverse of the burden of proof in Labor Procedure Law based on implementation of the Code of Consumer Protection, protective principle, principle of pre-establishment of proof and principle of the aptitude for proof. It analyzes general aspects concerning the theory of dynamic distribution of the burden of proof, establishing concepts and distinctions between static distribution, judicial reversal and dynamic distribution of the burden of proof, addressing historical origins and incorporation of the theory in Comparative Law, grounds for implementation of dynamic distribution of the burden of proof on Brazilian Procedural Law (with emphasis on the fundamental right to proof, principle of substantive equality in the process, practice of the judges investigation powers, search for real truth and rule of Article 333, sole paragraph, II, of the Code of Civil Procedure) and legislative incorporation of the theory in the Brazilian Procedural Law, foreseen in the preliminary bill of law for the Brazilian Code of Class Actions, bill of law for the Public Civil Action and bill of law for the Code of Civil Procedure. Finally, it studies specifically the application of the theory of dynamic distribution of the burden of proof on the Labor Procedural Law, starting for her impacts on the Labor Procedure (fundamental right to proof, principle of substantive equality in the process and the rule of Article 852 - D of the Consolidation of Labor Laws), addressing objective criteria to application (subsidiarity, use of the judges investigation powers, judges maxims of experience, prohibition to encourage self-indulgence and to establish reverse probatio diabolica, with observance of the binomial inability/extreme difficulty of the employee in the production of proof-possibility/ease in the production for the employer , reasons for the decision, seal to supervening procedural burden), procedural moment suitable to dynamize, relation between procedural nullity and dynamic distribution, appropriate procedural tool to challenge the incidence of the theory, definition of the distribution rule of the burden of proof by the Courts and case studies of application of the dynamic distribution of the burden of proof, with critical examination of doctrine and jurisprudence, in the Individual Labor Procedural Law (addressing the following topics: working time, transportation ticket, salary equation, Brazilian s employment compensation funds credit (FGTS), dismissal, family allowance, labor-related accident, workplace bullying and sexual harassment, discrimination in work relations, employee\'s privacy and intimacy, public administrations subsidiary liability, economic group, labor succession, homestead right and gratuity procedure) and Labor Class Actions, with formulating legislative proposition by the end of the study.

Proof-carrying code is an application of software verification techniques to the problem of ensuring the safety of mobile code. However, previous proof-carrying code systems have assumed that mobile code will faithfully execute the instructions of the program. Realistic implementations of computing systems are susceptible to probabilistic behaviours that can alter the execution of a program in ways that can result in corruption or security breaches. We investigate the use of a probabilistic bytecode language to model deterministic programs that are executed on probabilistic computing systems. To model probabilistic safety properties, a probabilistic logic is adapted to out bytecode instruction language, and soundness is proven. A sketch of a completeness proof of the logic is also shown.