In contemporary formal theory of truth, model-theoretic and non-classical approaches have been dominant. I rather pursue the so-called classical axiomatic approaches toward truth and my dissertation begins by arguing for the classical axiomatic approach and against the others. The classical axiomatic approach inevitably leads to abandonment of the nave conception of truth and revision of the basic principles of truth derived from that nave conception such as the full T-schema. In the absence of the general guiding principles based on that nave conception, we need to conduct tedious but down-to-earth eld works' of various theories of truth by examining and comparing them from various points of view in searching for satisfactory theories of truth. As such attempt, I raise two new criteria for comparison of truth theories, make a proof-theoretic study of them in connection to the foundation of mathematics.

Neste trabalho, buscamos propor atividades e relacionar ações que o professor de Matemática pode adotar durante as aulas, com o objetivo de propiciar a melhora do nível de argumentação e prova de seus alunos da Educação Básica. Inicialmente, pesquisamos sobre as definições de prova sob a ótica do ensino de Matemática, em que concluímos que o desenvolvimento de argumentações e provas é fundamental para que os objetivos dos PCN sejam alcançados. Com análise das avaliações do PISA, notamos que, em geral, os estudantes brasileiros possuem baixo desempenho em relação as habilidades que envolvem generalizações e desenvolvimento de provas. Na tentativa de propor melhorias a esse cenário, acreditamos que o desenvolvimento de provas na Educação Básica não deve se restringir as demonstrações aceitas pela comunidade matemática. Para isso, o professor deve conhecer e aceitar os diversos tipos de provas apresentados por seus alunos. Nesse ponto, a formação do professor de Matemática é essencial. Por fim, desenvolvemos atividades e aplicamos em uma sala do 9º ano do Ensino Fundamental, o que possibilitou, após as análises, que realizássemos conclusões sobre as características das atividades que propiciam o desenvolvimento de provas e ações que possibilitam a melhora do nível de argumentação de nossos estudantes. / In this study e seek to propose activities and to relate actions that the Mathematics teacher can adopt during the classes, seeking to improve the level of argument and proof of his students of Middle and High School. Initially, we investigated the definitions of proof from the point of view of mathematics teaching, in which we concluded that the development of arguments and proofs is fundamental for the goals of PCN been achieved. With the analysis of the PISA assessments, we noticed that, in general, Brazilian students have poor performance in relation to the skills that involve generalizations and the development of proofs. In an attempt to propose improvements to this scenario, we believe that the development of proofs in Middle and High School should not be restricted to the demonstrations accepted by the mathematical community. About that, the teacher must know and accept the different types of proofs presented by his students. At this point, the courses to the Mathematics teachers, preservice and inservice, are essential. Finally, we developed activities and applied in a class of 9th grade students, which made it possible, after the analysis, to make conclusions about the characteristics of the activities that help to the development of proofs and actions that allow the improvement of argumentations level of our students

1 Abstract The title of the work: Burden of Proof in Civil Procedure The present diploma thesis deals with one of the few subjects, which are topical today, as in the past, in spite of all legislative changes - the burden of proof in the civil procedure. The burden of proof, which is the subject of this work, plays in the process of evidence an irreplaceable role, yet it is still a very underrated topic, which is not, in particular in legal theory, given appropriate attention. Legal theory is not too unified with regard to the burden of proof, the views of different authors on this institute differ. This is a very large, somewhat unclear issue. There are many theories regarding the functioning of the burden of proof and its distribution among the parties. The thesis does not claim to give an exhausting interpretation of this institute, as it is a very extensive issue, and its comprehensive processing would require at least the publication of a book, perhaps several books, but should outline the institute of the burden of proof and its function in the civil procedure. The burden of proof is not clearly defined in the legislation and the theory of burden of proof is very complicated and inconsistent, that is probably why there is a relatively extensive case-law of the courts, which increasingly emphasizes...

Thesis advisor: Olivier Boulnois / Thesis advisor: Stephen F. Brown / The Dissertation Text has Three Parts. Each paragraph is referred at the end to the Part it summarizes. My dissertation places Saint Anselm’s Ontological Argument within its original Neoplatonic context that should justify its validity. The historical thesis is that Anselm’s epistemology, underlying the Proslogion, the Monologion and De Veritate, was a natural, often unaccounted for, reflection of the essentially Neoplatonic vision that defined the pre-thirteenth century mental culture in Europe. (Introduction and Part I) This thesis is shown through the reception of Anselm’s argument by 27 XIIIth-XIVth century thinkers, whose reading of it exhibits a gradual weakening of Neoplatonic premises up to a complete change of paradigm towards the XIVth century, the first reason being the specificity of the Medieval reception of Aristotle’s teaching on first principles that is the subject of Posterior Analytics (Part II), and the second reason being the specificity of the Medieval reception of Dionysius the Areopagite (Part III, see sub-thesis 4 below). The defense of this main historical thesis aims at proving three systematic sub-theses, including a further historical sub-thesis. The Three Systematic Sub-Theses: 1) The inadequacy of rationalist and idealist epistemology in reaching and providing apodictic truths (the chief one of which is God’s existence) with ultimate ontic grounding, as well as the inadequacy of objectivistic metaphysics that underlies these epistemologies, calls for another, non-objectifying epistemic paradigm offered by the Neoplatonic (Proclian theorem of transcendence) apophatic and supra-discursive logic (kenotic epistemology) that should be a better method to achieve certainty, because of its ability to found logic in its ontic source and thus envisage thought as an experience and a mode of being in which it is grounded. Within such a dialectic, there cannot be any opposition or division either between being and thought, or between faith and reason, faith being an ontic ground of reason’s activity defined as self-transcendence. The argument of the Proslogion is thus an instance of logic that transcends itself into its own principle – into ‘that than which nothing greater can be conceived’. Such an epistemological vision is also supported by contemporary epistemology (Russell’s Paradox and Gödel’s Incompleteness Theorem) (Introduction and Part I) 2) In virtue of this apophatic and supra-discursive vision, God’s existence, thought by human mind (as expressed in the argument of the Proslogion), happens to be a common denominator between God’s inaccessible essence and the created essence of human mind, so that human consciousness can be defined as ‘con-science’ – the mind experiencing its own being as co-knowledge with God that forges being as such. (Part I) 3) However, God’s existence as a common denominator between God’s essence and the created essence of human mind cannot be legitimately accommodated within the XIIIth-XIVth century epistemology and metaphysics because of the specificity of relation between God’s essence and His attributes, typical of Medieval scholasticism and as stated by Peter Lombard and Thomas Aquinas. If this relation is kept, while at the same time God’s existence is affirmed as immanent to the human mind (God as the first object of intellect), God’s transcendence is sacrificed and He becomes subject to metaphysics (Scotus’ nominal univocity of being). In order to achieve real univocity between the existence of human thinking and God’s existence, one needs a relation between God’s essence and His attributes that would allow a real participation of the created in the uncreated. The configuration of such a relation, however, needs the distinction between God’s essence and His energies that Western Medieval thought did not know, but that is inherent to the Neoplatonic epistemic tradition persisting through the Eastern Church theologians and Dionysius the Areopagite up to Gregory Palamas. (Part III) Another Historical Sub-Thesis: 4) One of the reasons why Medieval readers of Anselm’s Proslogion misread it in the Aristotelian key, was that they did not have access to the original work of Dionysius the Areopagite, in which the said distinction between God’s essence and His energies is present. This is due to the fact that the Medievals read Dionysius through Eriugena’s translation. However, Eriugena was himself influenced by Augustine’s De Trinitate that exhibits an essentialist theology: in fact, it places ideas within God’s essence, which yields the notion of the created as a mere similitude, not real participation, and which ultimately makes the vision (knowledge) of God possible only in the afterlife. Since already with Augustine the relation between grace and nature is modified (grace becomes a created manifestation of God, instead of being His uncreated energy), God’s essence remains incommunicable. Similarly, God’s existence is not in any way immanent to the created world, of which the created human intellect is a part, so that it remains as transcendent to the human mind as is His incommunicable essence. This should explain why for the Medievals analogy, and eventually univocity, was the only way to say something about God, and also why they mostly could not read Anselm’s Proslogion otherwise than either in terms of propositional or modal logic. (Part III) The dissertation concludes that whilst Anselm’s epistemology in the Proslogion is an instance of Neoplatonic metaphysical tradition, the question of the possibility of certainty in epistemology, as well as the possibility of metaphysics as such, depends on the possibility of real communicability between the immanence of human predicating mind and the transcendence of God’s essence through His trans-immanent existence.

Thesis advisor: Hideo Konishi / Becker (1968) provides a formal framework for analyzing various policies in criminal law. Within this framework there are potential criminals, who have varying benefits from committing an illegal act. They are subject to sanctions when they are caught and are found guilty for committing such acts. Accordingly, increased expected sanctions lead to greater deterrence. There are also costs associated with achieving such deterrence. Hence, there are optimal policy variables which balance costs and gains associated with increased deterrence. In my dissertation, in five independent but closely related essays, I address various issues related to criminal law by making use of optimal crime and deterrence models, which are similar to Becker (1968). First, I analyze the standard of proof in criminal trials and extend a justification as to why there are higher standards of proof in criminal trials versus civil trials. Next, I introduce the concept of mixed warning strategies, and justify the use of mixed as well as pure warning strategies in law enforcement. In a related essay, I show that it is optimal to punish repeat offenders more severely than first time offenders, provided that offenders gain experience in evading detection by committing offenses. In my fourth essay, I identify reasons as to why it is welfare improving to allow individuals to self-report conduct crimes. Finally, I propose a simple framework to incorporate the concept of remorse in the economic analysis of criminal law, and show that the Beckerian maximal fine result need not hold when some individuals feel remorse. / Thesis (PhD) — Boston College, 2010. / Submitted to: Boston College. Graduate School of Arts and Sciences. / Discipline: Economics.

O desenvolvimento tecnológico que se apresenta no dia-a-dia, mediante o aprimoramento de aparelhos domésticos, de videogames, de celulares, de computadores, de televisores, etc. é da mesma forma, porém paulatinamente, inserido no judiciário. Hoje é possível, por meio da videoconferência, percorrer centenas de quilômetros sem se deslocar, fazendo com que a distancia entre juízes e testemunhas ou réus seja limitada à distancia entre esses sujeitos e o aparelho de vídeo e televisão instalado em penitenciárias e fóruns. Outrossim, prestigia-se a dignidade da pessoa humana ao evitar a revitimização de crianças e adolescentes vítimas ou testemunhas de violência, diferenciando-as, nos termos do preconizado pela Constituição Federal, dos adultos, no decorrer do processo judicial. Por outro lado, o desenvolvimento alcança também as organizações criminosas, fazendo com que essas se tornem cada vez mais ameaçadoras à segurança pública, dificultando a produção de provas em seu desfavor, pelo que alguns Tribunais passaram a aceitar, de forma ainda polêmica, a produção de provas por meio de testemunha indireta e de testemunha anônima. Com todas essas transformações afetando diretamente o judiciário, e face ao surgimento de novas formas de se produzir provas consolidadas no direito, como é o caso da prova testemunhal, surge a necessidade de se fazer uma análise da admissibilidade desses novos meios de produção probatória. A análise de admissibilidade é feita inicialmente por meio de um estudo da tipicidade e dos elementos típicos da prova testemunhal como concebida no Código de Processo Penal atual. Após estabelecido o parâmetro, analisa-se os termos em que vêm sendo produzidas as novas formas de produção de prova testemunhal. Se essas estiverem de acordo com os elementos típicos da prova testemunhal, devem ser aceitas no ordenamento brasileiro como prova testemunhal típica. Se, por outro lado, os novos meios de produção probatória derivados da prova testemunhal mostrarem-se em desacordo com os elementos típicos da prova testemunhal, não poderão ser aceitos no ordenamento, exceto se não representarem prejuízo às partes. / The technological development that is presented in day-to-day, by upgrading household appliances, video games, cell phones, computers, televisions, etc. is in the same way, but gradually, inserted in the judiciary. Today it is possible, through video conferencing, travel hundreds of miles without moving, making the distance between judges and witnesses or defendants is limited to the distance between these subjects and the videocamera and television set in prisons and forums. Furthermore, honors the dignity of the human person to avoid revictimization of child victims or witnesses of violence , differentiating them, as recommended by the Federal Constitution, of the adults, in the course of judicial proceedings. Moreover, the development also reaches criminal organizations, making these become an increasingly threat to public security , dificulting the production of evidence in their disfavor, that´s why some courts have come to accept, in a still polemic form, the production of evidence through indirect and anonymous witness testimony. With all these changes directly affecting the judiciary, and with the emergence of new ways to produce consolidated evidence, as is the case of testimonial evidence, there is a need to do an analysis of the admissibility of these new means of evidentiary production. The analysis of admissibility is initially done through a study of typicality and typical elements of testimonial evidence as conceived in the current Code of Criminal Procedure. After the parameter is set, starts the analyze of the terms that are being produced the new forms of production of testimonial evidence. If these are in agreement with the typical elements of testimonial evidence, they should be accepted in the Brazilian system as typical witnesses. If, on the other hand, the new means of production derived from testimony show themselves against the typical elements of testimony, these can´t be accepted in the order, except if they do not represent harm to the parties.

Dependent type theories are a kind of mathematical foundations investigated both for the formalisation of mathematics and for reasoning about programs. They are implemented as the kernel of many proof assistants and programming languages with proofs (Coq, Agda, Idris, Dedukti, Matita, etc). Dependent types allow to encode elegantly and constructively the universal and existential quantifications of higher-order logics and are therefore adapted for writing logical propositions and proofs. However, their usage is not limited to the area of pure logic. Indeed, some recent work has shown that they can also be powerful for driving the construction of programs. Using more precise types not only helps to gain confidence about the program built, but it can also help its construction, giving rise to a new style of programming called Type-Driven Development. However, one difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories (like CIC and ML) from the fact that in a non-empty context, the propositional equality allows us to prove as equal (with the induction principles) terms that are not judgementally equal, which implies that the typechecker can't always obtain equality proofs by reduction. As far as possible, we would like to solve such proof obligations automatically, and we absolutely need it if we want dependent types to be use more broadly, and perhaps one day to become the standard in functional programming. In this thesis, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. However, the method that we follow is independent from the language being used, and this work could be reproduced in any dependently-typed language. We present an original type-safe reflection mechanism, where reflected terms are indexed by the original Idris expression that they represent, and show how it allows us to easily construct and manipulate proofs. We build a hierarchy of correct-by-construction tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs. Finally, and as a conclusion, we discuss the trust we can have in such machine-checked proofs.

EVIDENCE IN TAX PROCEEDINGS Abstract The purpose of the thesis is on one hand to provide an overall view of the issue of burden of proof in tax proceedings. On the other hand the thesis gives a detailed look into unclear and problematic provisions of the Tax Code concerning the burden of proof of tax subjects as well as that of tax administrators. The reason for my analysis is that number of questions related to the burden of proof in tax proceedings are very often matter of disputes between tax subjects and tax administrators which in many cases has to be decided by the Czech Supreme Administrative Court. The thesis is composed of four chapters, each of them dealing with different aspects of evidence. Chapter One is introductory and deals with evidence in proceedings in general. It also defines basic terminology used in the thesis such as evidence, basic principles of process, burden of production or burden of persuasion. The Chapter Two explains specifics of evidence in tax proceedings. Chapter Three deals with the definition of evidence and mentions different types of evidence in tax proceedings. Chapter Four is focused on the key issue of evidence in tax proceedings - the concept of burden of proof. The chapter consists of five parts. Part One concerns burden of proof of taxpayers while Part Two looks...

The specification and verification of communicating systems has captured increasing interest in the last decades. CCS, a Calculus of Communicating Systems [Milner 89a], was especially designed to help this enterprise; it is widely used in both industry and academia. Most efforts to automate the use of CCS for verification have centered around the explicit construction of a bisimulation [Park 81]. This approach, however, presents severe limitations to deal with systems that contain infinite states (e.g. systems with evolving structure [Milner 89a] or that comprise a finite but arbitrary number of components (e.g. systems with inductive structure [Milner 89a]). There is an alternative approach to verification, based on equational reasoning, which does not exhibit such limitations. This formulation, however, introduces significant proof search control issues, and, hence, has remained far less explored. This thesis investigates the use of explicit proof plans [Bundy 88] for problems of automatic verification in the context of CCS. We have conducted the verification task using equational reasoning, and centred on infinite state systems, and parameterised systems. A parameterised system, e.g. a system with inductive structure, circumscribes a family of CCS systems, which have fixed struture and finitely many states. To reason about theses systems, we have adopted Robin Milner's approach [Milner 89a], which advocates the use of induction to exploit the structure and/or the behavior of a system during its verification. To automate this reasoning, wehave used proof plans for induction [Bundy 88]- built within CLAM [Bundy et al 90b], and extended it with special CCS proof plans. We have implemented a verification planner by adding these special proof plans to CLAM. The system handles the search control problems prompted by CCS verification satisfactorily, though it is not complete. Moreover, the system is capable of dealing with the verification of finite state systems, infinite state systems, and parameterised systems, hence, providing a uniform method to analyse CCS systems, regardless of their state space. Our results are encouraging: the verification planner has been successfully tested on a number of examples drawn from the litereature. We have planned proofs of conjectures that are outside the domain of existing verification methods. Furthernore; the verification planning is fully automated. Because of this, even though the verification plan has still got plenty of room for improvement, we can state that proof planning can handle the equational verication of CCS systems, and, therefore, advocate its use within this interesting field.

This thesis is about automated reasoning in quantified modal and temporal logics, with an application to formal methods. Quantified modal and temporal logics are extensions of classical first-order logic in which the notion of truth is extended to take into account its necessity or equivalently, in the temporal setting, its persistence through time. Due to their high complexity, these logics are less widely known and studied than their propositional counterparts. Moreover, little so far is known about their mechanisability and usefulness for formal methods. The relevant contributions of this thesis are threefold: firstly, we devise a sound and complete set of sequent calculi for quantified modal logics; secondly, we extend the approach to the quantified temporal logic of linear, discrete time and develop a framework for doing automated reasoning via Proof Planning in it; thirdly, we show a set of experimental results obtained by applying the framework to the problem of Feature Interactions in telecommunication systems. These results indicate that (a) the problem can be concisely and effectively modeled in the aforementioned logic, (b) proof planning actually captures common structures in the related proofs, and (c) the approach is viable also from the point of view of efficiency.