This thesis is an investigation into the foundations of reasoning with default rules as presented by Reiter in his seminal 1980 article: `A Logic for Default Reasoning'. In being such, it opens up with a critical appraisal of the logical underpinnings of Reiter's presentation of the main elements of reasoning with default rules. More precisely, following Reiter's presentation, it discusses the concept of a default rule in comparison with that of a rule of inference, the concept of an extension in comparison with that of a theory, and the concept of `being a consequence of' for reasoning with default rules. Contrary to the commonly perceived view, the argument put forth is that such a context does not provide sensible logical foundation for reasoning with default rules. As a result, this thesis argues for an alternative interpretation to what is captured by default rules, what is captured by extensions, and what `being a consequence of' for reasoning with default rules amounts to. In particular, it proposes to treat default rules as premiss-like objects standing for assertions made tentatively, to treat extensions as interpretation structures of a syntactical kind, and to bring the concept of `being a consequence of' for reasoning with default rules into the foreground by formulating a suitable notion of an entailment relation and its ensuing logical system. Accounting for the fact that in any logical system it is important to have at hand mechanisms for formulating proofs and for structuring large theories, this thesis presents a tableaux based proof calculus for reasoning with default rules and it explores some mappings notions related to the structuring of default presentations, i.e., presentations in the context of reasoning with default rules. / Thesis / Doctor of Philosophy (PhD) / This thesis is an investigation into the foundations of reasoning with default rules as presented by Reiter in his seminal 1980 article: `A Logic for Default Reasoning'. A first very general problem definition for this Ph.D. thesis is raised by the following question: Can reasoning with default rules, as presented in Reiter's seminal 1980 article: `A Logic for Default Reasoning', be understood as a logic for non-monotonic reasoning? This thesis presents a rationale for the formulation of such a question and a possible answer for it. On the more technical side, this thesis presents a proof calculus for a particular formulation of a logic for reasoning with default rules, as well as some mapping concepts for structuring presentations defined on this logic.

This thesis describes a decision and minimization procedure for modal logic. The decision procedure answers the question of whether there exists a satisfying pointed model for a formula which obeys user-specified first-order conditions on the underlying frame. Then the minimization procedure produces a minimal model with respect to the number of worlds that satisfies the desired formula while obeying the requisite conditions on the underlying frame. A proof of correctness for the decision and minimization procedures is supplied, as well as a description of an implementation built upon the Enfragmo model expansion solver. / Graduate / 0984 / 0318 / wbkboyer@gmail.com

The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library. / Thesis / Doctor of Philosophy (PhD) / The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library.

By extending Husserl’s own historico-critical study to include the conceptual mathematics of more contemporary times – specifically category theory and its emphatic development since the second half of the 20th century – this paper claims that the delineation between mathematics and philosophy must be completely revisited. It will be contended that Husserl’s phenomenological work was very much influenced by the discoveries and limitations of the formal mathematics being developed at Göttingen during his tenure there and that, subsequently, the rôle he envisaged for his material a priori science is heavily dependent upon his conception of the definite manifold. Motivating these contentions is the idea of a mathematics which would go beyond the constraints of formal ontology and subsequently achieve coherence with the full sense of transcendental phenomenology. While this final point will be by no means proven within the confines of this paper it is hoped that the very fact of opening up for the possibility of such an idea will act as a supporting argument to the overriding thesis that the relationship between mathematics and phenomenology must be problematised.

O objetivo principal da tese é examinar se, na filosofia prática de Immanuel Kant, estariam já contidas distintas variantes da ideia de universalizabilidade, mais especificamente as variantes de Richard Mervyn Hare, Kurt Baier, Marcus George Singer e Jürgen Habermas, com vistas a determinar se a teoria do discurso prático racional de Robert Alexy poderia ser designada como kantiana. O objetivo secundário da tese é examinar se a ideia de universalizabilidade, tal como desenvolvida na lógica formal e na ética de orientação kantiana, pode ser empregada com sucesso na fundamentação filosófica do princípio jurídico da igualdade e da vinculatividade dos precedentes judiciais, bem como apresentar argumentos baseados na universalizabilidade e nos precedentes para a solução de três recursos extraordinários, com repercussão geral reconhecida, que estão pendentes de julgamento pelo Supremo Tribunal Federal brasileiro: Recursos Extraordinários no 611.874, no 639.138 e no 710.293. Os métodos empregados foram o lógico-analítico, o hermenêutico e o comparativo, incluindo também pesquisa bibliográfica, jurisprudencial e legislativa. Os principais resultados obtidos foram estes: (i) do ponto de vista da lógica formal, a universalizabilidade pode ser situada no âmbito das regras de operação do cálculo de predicados de primeira ordem; (ii) com relação às diferentes formulações do imperativo categórico de Kant, a Fórmula IIIa (Reino dos Fins) parece a mais abrangente, ao compreender a forma da ação moral (a lei universal) e a matéria da ação moral (as pessoas como fins em si mesmas); (iii) em seus aspectos essenciais, as variantes da universalizabilidade de Hare, Baier, Singer e Habermas podem ser reconduzidas ao imperativo categórico kantiano; (iv) na filosofia do direito e do estado de Kant, a doutrina da dação de leis dupla explica a diferença entre a dação de leis ética e a dação de leis jurídica com base na diferença da “mola propulsora” (Triebfeder); (v) a existência de uma estreita ligação entre os conceitos de direito (incluindo a possibilidade de coerção externa), de universalizabilidade e de igualdade (na aplicação do direito e no estabelecimento do direito) foi demonstrada; (vi) os dois conceitos fundamentais da teoria do precedente – stare decisis e ratio decidendi – podem ser reconduzidos à ideia de universalizabilidade; (vii) tanto os argumentos baseados na utilização de precedentes, quanto o argumento da universalizabilidade, podem oferecer importantes contribuições para a solução de casos concretos, pendentes de julgamento nos tribunais brasileiros. As conclusões alcançadas a partir dos resultados são que as variantes da ideia de universalizabilidade de Hare, Baier, Singer e Habermas podem, em seus aspectos essenciais, ser reconduzidas à filosofia prática de Kant, demonstrando também a compatibilidade da teoria do discurso prático racional de Alexy com esta filosofia. / The main objective of the thesis is to examine whether in Immanuel Kant’s practical philosophy distinct variants of the idea of universalizability are already contained, in particular Richard Mervyn Hare’s, Kurt Baier’s, Marcus George Singer’s and Jürgen Habermas’ variants, with a view to determine whether Robert Alexy’s theory of rational practical discourse could be construed as Kantian. The secondary objective of the thesis is to examine whether the idea of universalizability, such as developed in formal logic and ethics of Kantian orientation, can be employed successfully in the philosophical foundation of the legal principle of equality and of the binding character of judicial precedent, as well as to present arguments based on universalizability and precedent for the solution of three extraordinary appeals, with recognized general repercussion, which are pending judgment in the Brazilian Federal Supreme Court: Extraordinary Appeals n. 611.874, n. 639.138 and n. 710.293. The methods employed were the logical-analytic, the hermeneutic and the comparative, including also bibliographical, case law and legislative review. The main results obtained were as follows: (i) from the viewpoint of formal logic, universalizability can be located within the domain of operation rules of first order predicate calculus; (ii) in relation to the different formulas of Kant’s categorical imperative, the Formula IIIa (Kingdom of Ends) seems the more inclusive, by comprehending the form of moral action (the universal law) and the matter of moral action (the people as ends in themselves); ( (iii) in their essential aspects, Hare’s, Baier’s, Singer’s and Habermas’ variants of universalizability can be reduced to the Kantian categorical imperative; (iv) in Kant’s philosophy of law and state, the double law-giving doctrine explains the difference between the ethical law-giving and legal law-giving based on the difference between “incentive” (Triebfeder); (v) the existence of a close link between the concepts of law (including the possibility of external coercion), universalizability and equality (in the application of law and in the establishment of law) was demonstrated; (vi) the two fundamental concepts of the theory of precedent – stare decisis and ratio decidendi – can be reduced to the idea of universalizability; (vii) both arguments based on the utilization of precedent and the argument of universalizability can offer an important contribution to the solution of concrete cases, pending judgment in Brazilian courts. The conclusions obtained from the results are that Hare’s, Baier’s, Singer’s and Habermas’ variants of the idea of universalizability can, in their essential aspects, be reduced to Kant’s practical philosophy, also demonstrating the compatibility between Alexy’s theory of rational practical discourse and that philosophy.

O objetivo principal da tese é examinar se, na filosofia prática de Immanuel Kant, estariam já contidas distintas variantes da ideia de universalizabilidade, mais especificamente as variantes de Richard Mervyn Hare, Kurt Baier, Marcus George Singer e Jürgen Habermas, com vistas a determinar se a teoria do discurso prático racional de Robert Alexy poderia ser designada como kantiana. O objetivo secundário da tese é examinar se a ideia de universalizabilidade, tal como desenvolvida na lógica formal e na ética de orientação kantiana, pode ser empregada com sucesso na fundamentação filosófica do princípio jurídico da igualdade e da vinculatividade dos precedentes judiciais, bem como apresentar argumentos baseados na universalizabilidade e nos precedentes para a solução de três recursos extraordinários, com repercussão geral reconhecida, que estão pendentes de julgamento pelo Supremo Tribunal Federal brasileiro: Recursos Extraordinários no 611.874, no 639.138 e no 710.293. Os métodos empregados foram o lógico-analítico, o hermenêutico e o comparativo, incluindo também pesquisa bibliográfica, jurisprudencial e legislativa. Os principais resultados obtidos foram estes: (i) do ponto de vista da lógica formal, a universalizabilidade pode ser situada no âmbito das regras de operação do cálculo de predicados de primeira ordem; (ii) com relação às diferentes formulações do imperativo categórico de Kant, a Fórmula IIIa (Reino dos Fins) parece a mais abrangente, ao compreender a forma da ação moral (a lei universal) e a matéria da ação moral (as pessoas como fins em si mesmas); (iii) em seus aspectos essenciais, as variantes da universalizabilidade de Hare, Baier, Singer e Habermas podem ser reconduzidas ao imperativo categórico kantiano; (iv) na filosofia do direito e do estado de Kant, a doutrina da dação de leis dupla explica a diferença entre a dação de leis ética e a dação de leis jurídica com base na diferença da “mola propulsora” (Triebfeder); (v) a existência de uma estreita ligação entre os conceitos de direito (incluindo a possibilidade de coerção externa), de universalizabilidade e de igualdade (na aplicação do direito e no estabelecimento do direito) foi demonstrada; (vi) os dois conceitos fundamentais da teoria do precedente – stare decisis e ratio decidendi – podem ser reconduzidos à ideia de universalizabilidade; (vii) tanto os argumentos baseados na utilização de precedentes, quanto o argumento da universalizabilidade, podem oferecer importantes contribuições para a solução de casos concretos, pendentes de julgamento nos tribunais brasileiros. As conclusões alcançadas a partir dos resultados são que as variantes da ideia de universalizabilidade de Hare, Baier, Singer e Habermas podem, em seus aspectos essenciais, ser reconduzidas à filosofia prática de Kant, demonstrando também a compatibilidade da teoria do discurso prático racional de Alexy com esta filosofia. / The main objective of the thesis is to examine whether in Immanuel Kant’s practical philosophy distinct variants of the idea of universalizability are already contained, in particular Richard Mervyn Hare’s, Kurt Baier’s, Marcus George Singer’s and Jürgen Habermas’ variants, with a view to determine whether Robert Alexy’s theory of rational practical discourse could be construed as Kantian. The secondary objective of the thesis is to examine whether the idea of universalizability, such as developed in formal logic and ethics of Kantian orientation, can be employed successfully in the philosophical foundation of the legal principle of equality and of the binding character of judicial precedent, as well as to present arguments based on universalizability and precedent for the solution of three extraordinary appeals, with recognized general repercussion, which are pending judgment in the Brazilian Federal Supreme Court: Extraordinary Appeals n. 611.874, n. 639.138 and n. 710.293. The methods employed were the logical-analytic, the hermeneutic and the comparative, including also bibliographical, case law and legislative review. The main results obtained were as follows: (i) from the viewpoint of formal logic, universalizability can be located within the domain of operation rules of first order predicate calculus; (ii) in relation to the different formulas of Kant’s categorical imperative, the Formula IIIa (Kingdom of Ends) seems the more inclusive, by comprehending the form of moral action (the universal law) and the matter of moral action (the people as ends in themselves); ( (iii) in their essential aspects, Hare’s, Baier’s, Singer’s and Habermas’ variants of universalizability can be reduced to the Kantian categorical imperative; (iv) in Kant’s philosophy of law and state, the double law-giving doctrine explains the difference between the ethical law-giving and legal law-giving based on the difference between “incentive” (Triebfeder); (v) the existence of a close link between the concepts of law (including the possibility of external coercion), universalizability and equality (in the application of law and in the establishment of law) was demonstrated; (vi) the two fundamental concepts of the theory of precedent – stare decisis and ratio decidendi – can be reduced to the idea of universalizability; (vii) both arguments based on the utilization of precedent and the argument of universalizability can offer an important contribution to the solution of concrete cases, pending judgment in Brazilian courts. The conclusions obtained from the results are that Hare’s, Baier’s, Singer’s and Habermas’ variants of the idea of universalizability can, in their essential aspects, be reduced to Kant’s practical philosophy, also demonstrating the compatibility between Alexy’s theory of rational practical discourse and that philosophy.

O objetivo principal da tese é examinar se, na filosofia prática de Immanuel Kant, estariam já contidas distintas variantes da ideia de universalizabilidade, mais especificamente as variantes de Richard Mervyn Hare, Kurt Baier, Marcus George Singer e Jürgen Habermas, com vistas a determinar se a teoria do discurso prático racional de Robert Alexy poderia ser designada como kantiana. O objetivo secundário da tese é examinar se a ideia de universalizabilidade, tal como desenvolvida na lógica formal e na ética de orientação kantiana, pode ser empregada com sucesso na fundamentação filosófica do princípio jurídico da igualdade e da vinculatividade dos precedentes judiciais, bem como apresentar argumentos baseados na universalizabilidade e nos precedentes para a solução de três recursos extraordinários, com repercussão geral reconhecida, que estão pendentes de julgamento pelo Supremo Tribunal Federal brasileiro: Recursos Extraordinários no 611.874, no 639.138 e no 710.293. Os métodos empregados foram o lógico-analítico, o hermenêutico e o comparativo, incluindo também pesquisa bibliográfica, jurisprudencial e legislativa. Os principais resultados obtidos foram estes: (i) do ponto de vista da lógica formal, a universalizabilidade pode ser situada no âmbito das regras de operação do cálculo de predicados de primeira ordem; (ii) com relação às diferentes formulações do imperativo categórico de Kant, a Fórmula IIIa (Reino dos Fins) parece a mais abrangente, ao compreender a forma da ação moral (a lei universal) e a matéria da ação moral (as pessoas como fins em si mesmas); (iii) em seus aspectos essenciais, as variantes da universalizabilidade de Hare, Baier, Singer e Habermas podem ser reconduzidas ao imperativo categórico kantiano; (iv) na filosofia do direito e do estado de Kant, a doutrina da dação de leis dupla explica a diferença entre a dação de leis ética e a dação de leis jurídica com base na diferença da “mola propulsora” (Triebfeder); (v) a existência de uma estreita ligação entre os conceitos de direito (incluindo a possibilidade de coerção externa), de universalizabilidade e de igualdade (na aplicação do direito e no estabelecimento do direito) foi demonstrada; (vi) os dois conceitos fundamentais da teoria do precedente – stare decisis e ratio decidendi – podem ser reconduzidos à ideia de universalizabilidade; (vii) tanto os argumentos baseados na utilização de precedentes, quanto o argumento da universalizabilidade, podem oferecer importantes contribuições para a solução de casos concretos, pendentes de julgamento nos tribunais brasileiros. As conclusões alcançadas a partir dos resultados são que as variantes da ideia de universalizabilidade de Hare, Baier, Singer e Habermas podem, em seus aspectos essenciais, ser reconduzidas à filosofia prática de Kant, demonstrando também a compatibilidade da teoria do discurso prático racional de Alexy com esta filosofia. / The main objective of the thesis is to examine whether in Immanuel Kant’s practical philosophy distinct variants of the idea of universalizability are already contained, in particular Richard Mervyn Hare’s, Kurt Baier’s, Marcus George Singer’s and Jürgen Habermas’ variants, with a view to determine whether Robert Alexy’s theory of rational practical discourse could be construed as Kantian. The secondary objective of the thesis is to examine whether the idea of universalizability, such as developed in formal logic and ethics of Kantian orientation, can be employed successfully in the philosophical foundation of the legal principle of equality and of the binding character of judicial precedent, as well as to present arguments based on universalizability and precedent for the solution of three extraordinary appeals, with recognized general repercussion, which are pending judgment in the Brazilian Federal Supreme Court: Extraordinary Appeals n. 611.874, n. 639.138 and n. 710.293. The methods employed were the logical-analytic, the hermeneutic and the comparative, including also bibliographical, case law and legislative review. The main results obtained were as follows: (i) from the viewpoint of formal logic, universalizability can be located within the domain of operation rules of first order predicate calculus; (ii) in relation to the different formulas of Kant’s categorical imperative, the Formula IIIa (Kingdom of Ends) seems the more inclusive, by comprehending the form of moral action (the universal law) and the matter of moral action (the people as ends in themselves); ( (iii) in their essential aspects, Hare’s, Baier’s, Singer’s and Habermas’ variants of universalizability can be reduced to the Kantian categorical imperative; (iv) in Kant’s philosophy of law and state, the double law-giving doctrine explains the difference between the ethical law-giving and legal law-giving based on the difference between “incentive” (Triebfeder); (v) the existence of a close link between the concepts of law (including the possibility of external coercion), universalizability and equality (in the application of law and in the establishment of law) was demonstrated; (vi) the two fundamental concepts of the theory of precedent – stare decisis and ratio decidendi – can be reduced to the idea of universalizability; (vii) both arguments based on the utilization of precedent and the argument of universalizability can offer an important contribution to the solution of concrete cases, pending judgment in Brazilian courts. The conclusions obtained from the results are that Hare’s, Baier’s, Singer’s and Habermas’ variants of the idea of universalizability can, in their essential aspects, be reduced to Kant’s practical philosophy, also demonstrating the compatibility between Alexy’s theory of rational practical discourse and that philosophy.

Title: Logic and cryptography Author: Bc.Vojtěch Wagner Department: Department of Algebra Supervisor: prof. RNDr. Jan Krajíček, DrSc. Abstract: This work is devoted to a study of a formal method of formalization of cryptographic constructions. It is based on defining a multi-sorted formal logic theory T composed of strings, integers and objects of sort k - k-ary functions. We allow some operations on them, formulate axioms, terms and formulas. We also have a special type of integers called the counting integers. It denotes the number of x from a given interval satisfying formula ϕ(x). It allows us to talk about probabilities and use terms of probability theory. The work first describes this theory and then it brings a formalization of the Goldreich-Levin theorem. The goal of this work is to adapt all needed cryptographic terms into the language of T and then prove the theorem using objects, rules and axioms of T. Presented definitions and principles are ilustrated on examples. The purpose of this work is to show that such theory is sufficiently strong to prove such cryptographic constructions and verify its correctness and security. Keywords: cryptography, protocol verifying, Soundness theorem, formal logic theory, the Goldreich-Levin theorem 1