Extending relAPS to first order logic

RelAPS is an interactive system assisting in proving relation-algebraic theorems. The aim of the system is to provide an environment where a user can perform a relation-algebraic proof similar to doing it using pencil and paper. The previous version of RelAPS accepts only Horn-formulas. To extend the system to first order logic, we have defined and implemented a new language based on theory of allegories as well as a new calculus. The language has two different kinds of terms; object terms and relational terms, where object terms are built from object constant symbols and object variables, and relational terms from typed relational constant symbols, typed relational variables, typed operation symbols and the regular operations available in any allegory. The calculus is a mixture of natural deduction and the sequent calculus. It is formulated in a sequent style but with exactly one formula on the right-hand side. We have shown soundness and completeness of this new logic which verifies that the underlying proof system of RelAPS is working correctly.

An Interactive Theorem Prover for First-Order Dynamic Logic

Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used.

Methodology in Economics: the Logic of Appraisal

This Paper Intends to Develop a Coherent Methodological Framework Concerned with the Appraisal of Scientific Theories in Economics, and Which Is Based on a Postulated Aim of Science. We First Define the Scope of a Methodological Inquiry (Precise Definition of What Is Meant by the Logic of Appraisal of Scientific Theories) and Review the Work of Popper and Lakatos in the Philosophy of Science. We Then Use Their Results to Develop a Rational Structure of Scientific Activity. We Identify and Analyse Both a Micro and Macro Framework for the Process of Appraisal and Single Out the Importance of So-Called 'Fundamental Assumptions' in Creating Externalities in the Appraisal Process Which Forces Us to Adop a Multi-Level Analysis. Special Attention Is Given to the Role and Significance of the Abstraction Process and the Use of Assumptions in General. the Proposed Structure of Scientific Activity Is Illustrated with Examples From Economics.

La genèse d'une classe de mots : les conjonctions dans la tradition (pré-)grammaticale de l'Antiquité grecque

La présente recherche porte sur la théorie des parties du discours dans l’Antiquité grecque et plus particulièrement sur la réflexion entourant les conjonctions. Le premier chapitre se concentre sur la définition de la conjonction trouvée dans la Poétique d’Aristote, de même que sur les autres passages du corpus aristotélicien qui permettent de mieux cerner les contours d’une entité grammaticale encore mal définie. Le second chapitre porte sur la conjonction dans les recherches logico-grammaticales de l’école stoïcienne. La définition stoïcienne de la conjonction, de même que les différentes catégories de conjonctions identifiées par les Stoïciens sont examinées. Le rôle central des conjonctions au sein de la théorie stoïcienne des propositions complexes est souligné et met en lumière l’interrelation étroite entre la logique et la grammaire à ce point du développement de la théorie grammaticale. Le chapitre final porte sur la définition et les catégories de conjonctions trouvées dans la Tekhnè grammatikè, un bref manuel de grammaire attribué au philologue alexandrin Denys le Thrace. L’influence de la théorie stoïcienne des propositions complexes sur cette première tentative de systématisation grammaticale est mise en lumière, de même que l’interférence de préoccupations philologiques.

Phronesis and Energeia : a reading of Heidegger's early appropriation of Aristotelian Phronesis (1922-24) in the light of Energeia

L’objectif de cette thèse est d’élucider l’intention, la pertinence et la cohérence de l’appropriation par Heidegger des concepts principaux de la philosophie pratique aristotélicienne dans ses premiers cours. Notre analyse portera principalement sur les notions clefs d’energeia et de phronēsis. La première section de la thèse est préparatoire : elle est consacrée à une analyse étroite des textes pertinents de l’Éthique à Nicomaque, mais aussi de la Métaphysique, en discussion avec d’autres commentateurs modernes. Cette analyse jette les fondations philologiques nécessaires en vue d’aborder les audacieuses interprétations de Heidegger sur une base plus ferme. La deuxième et principale section consiste en une discussion de l’appropriation ontologique de l’Éthique à Nicomaque que Heidegger entreprend de 1922 à 1924, à partir des textes publiés jusqu’à ce jour et en portant une attention spéciale à Métaphysique IX. Le résultat principal de la première section est un aperçu du caractère central de l’energeia pour le projet d’Aristote dans l’Éthique à Nicomaque et, plus spécifiquement, pour sa compréhension de la praxis, qui dans son sens original s’avère être un mode d’être des êtres humains. Notre analyse reconnaît trois traits essentiels de l’energeia et de la praxis, deux desquels provenant de l’élucidation aristotélicienne de l’energeia dans Métaphysique IX 6, à savoir son immédiateté et sa continuité : energeia exprime l’être comme un « accomplissement immédiat mais inachevé ». L’irréductibilité, troisième trait de l’energeia et de la praxis, résulte pour sa part de l’application de la structure de l’energeia à la caractérisation de la praxis dans l’Éthique à Nicomaque, et du contraste de la praxis avec la poiēsis et la theōria. Ces trois caractéristiques impliquent que la vérité pratique ― la vérité de la praxis, ce qui est l’ « objet » de la phronēsis ― ne peut être à proprement parler possédée et ainsi transmise : plus qu’un savoir, elle se révèle surtout comme quelque chose que nous sommes. C’est ce caractère unique de la vérité pratique qui a attiré Heidegger vers Aristote au début des années 1920. La deuxième section, consacrée aux textes de Heidegger, commence par la reconstruction de quelques-uns des pas qui l’ont conduit jusqu’à Aristote pour le développement de son propre projet philosophique, pour sa part caractérisé par une profonde, bien qu’énigmatique combinaison d’ontologie et de phénoménologie. La légitimité et la faisabilité de l’appropriation clairement ontologique de l’Éthique à Nicomaque par Heidegger est aussi traitée, sur la base des résultats de la première section. L’analyse de ces textes met en lumière la pénétrante opposition établie par Heidegger entre la phronēsis et l’energeia dans son programmatique Natorp Bericht en 1922, une perspective qui diverge fortement des résultats de notre lecture philologique d’Aristote dans la première section. Cette opposition est maintenue dans nos deux sources principales ― le cours du semestre d’hiver 1924-25 Platon: Sophistes, et le cours du semestre d’été 1924 Grundbegriffe der aristotelischen Philosophie. Le commentaire que Heidegger fait du texte d’Aristote est suivi de près dans cette section: des concepts tels que energeia, entelecheia, telos, physis ou hexis ― qui trouvent leur caractérisation ontologique dans la Métaphysique ou la Physique ― doivent être examinés afin de suivre l’argument de Heidegger et d’en évaluer la solidité. L’hypothèse de Heidegger depuis 1922 ― à savoir que l’ontologie aristotélicienne n’est pas à la hauteur des aperçus de ses plus pénétrantes descriptions phénoménologiques ― résulte en un conflit opposant phronēsis et sophia qui divise l’être en deux sphères irréconciliables qui auraient pour effet selon Heidegger de plonger les efforts ontologiques aristotéliciens dans une impasse. Or, cette conclusion de Heidegger est construite à partir d’une interprétation particulière de l’energeia qui laisse de côté d’une manière décisive son aspect performatif, pourtant l’un des traits essentiels de l’energeia telle qu’Aristote l’a conçue. Le fait que dans les années 1930 Heidegger ait lui-même retrouvé cet aspect de l’energeia nous fournit des raisons plus fortes de mettre en doute le supposé conflit entre ontologie et phénoménologie chez Aristote, ce qui peut aboutir à une nouvelle formulation du projet heideggérien.

Bounding of switching activity in logic circuits

Thèse diffusée initialement dans le cadre d'un projet pilote des Presses de l'Université de Montréal/Centre d'édition numérique UdeM (1997-2008) avec l'autorisation de l'auteur.

Realization of Optical Logic Gates Using the Thermal Lens Effect

A sensitive method based on the principle of photothermal phenomena to realize optical logic gates is presented. A dual beam thermal lens method using low power cw lasers in a dye-doped polymer can be very effectively used as an alternate technique to perform the logical function such as NAND, AND and OR.

A new look at reversible logic implementation of decimal adder

Reversibility plays a fundamental role when logic gates such as AND, OR, and XOR are not reversible. computations with minimal energy dissipation are considered. Hence, these gates dissipate heat and may reduce the life of In recent years, reversible logic has emerged as one of the most the circuit. So, reversible logic is in demand in power aware important approaches for power optimization with its circuits. application in low power CMOS, quantum computing and A reversible conventional BCD adder was proposed in using conventional reversible gates.

Performance analysis of double digit decimal multiplier on various FPGA logic families

Decimal multiplication is an integral part of financial, commercial, and internet-based computations. This paper presents a novel double digit decimal multiplication (DDDM) technique that performs 2 digit multiplications simultaneously in one clock cycle. This design offers low latency and high throughput. When multiplying two n-digit operands to produce a 2n-digit product, the design has a latency of (n / 2) 1 cycles. The paper presents area and delay comparisons for 7-digit, 16-digit, 34-digit double digit decimal multipliers on different families of Xilinx, Altera, Actel and Quick Logic FPGAs. The multipliers presented can be extended to support decimal floating-point multiplication for IEEE P754 standard

Quick Addition of Decimals Using Reversible Conservative Logic

In recent years, reversible logic has emerged as one of the most important approaches for power optimization with its application in low power CMOS, nanotechnology and quantum computing. This research proposes quick addition of decimals (QAD) suitable for multi-digit BCD addition, using reversible conservative logic. The design makes use of reversible fault tolerant Fredkin gates only. The implementation strategy is to reduce the number of levels of delay there by increasing the speed, which is the most important factor for high speed circuits.

Automated synthesis of delay-reduced Reed-Muller universal logic module networks

This paper presents a new approach to implement Reed-Muller Universal Logic Module (RM-ULM) networks with reduced delay and hardware for synthesizing logic functions given in Reed-Muller (RM) form. Replication of single control line RM-ULM is used as the only design unit for defining any logic function. An algorithm is proposed that does exhaustive branching to reduce the number of levels and modules required to implement any logic function in RM form. This approach attains a reduction in delay, and power over other implementations of functions having large number of variables.

A contextual-logic extension of TOSCANA

The aim of this paper is to indicate how TOSCANA may be extended to allow graphical representations not only of concept lattices but also of concept graphs in the sense of Contextual Logic. The contextual-logic extension of TOSCANA requires the logical scaling of conceptual and relatioal scales for which we propose the Peircean Algebraic Logic as reconstructed by R. W. Burch. As graphical representations we recommend, besides labelled line diagrams of concept lattices and Sowa's diagrams of conceptual graphs, particular information maps for utilizing background knowledge as much as possible. Our considerations are illustrated by a small information system about the domestic flights in Austria.

Asymptotically Zero Energy Computing Using Split-Level Charge Recovery Logic

The dynamic power requirement of CMOS circuits is rapidly becoming a major concern in the design of personal information systems and large computers. In this work we present a number of new CMOS logic families, Charge Recovery Logic (CRL) as well as the much improved Split-Level Charge Recovery Logic (SCRL), within which the transfer of charge between the nodes occurs quasistatically. Operating quasistatically, these logic families have an energy dissipation that drops linearly with operating frequency, i.e., their power consumption drops quadratically with operating frequency as opposed to the linear drop of conventional CMOS. The circuit techniques in these new families rely on constructing an explicitly reversible pipelined logic gate, where the information necessary to recover the energy used to compute a value is provided by computing its logical inverse. Information necessary to uncompute the inverse is available from the subsequent inverse logic stage. We demonstrate the low energy operation of SCRL by presenting the results from the testing of the first fully quasistatic 8 x 8 multiplier chip (SCRL-1) employing SCRL circuit techniques.

Reasoning about Temporal Context using Ontology and Abductive Constraint Logic Programming

The underlying assumptions for interpreting the meaning of data often change over time, which further complicates the problem of semantic heterogeneities among autonomous data sources. As an extension to the COntext INterchange (COIN) framework, this paper introduces the notion of temporal context as a formalization of the problem. We represent temporal context as a multi-valued method in F-Logic; however, only one value is valid at any point in time, the determination of which is constrained by temporal relations. This representation is then mapped to an abductive constraint logic programming framework with temporal relations being treated as constraints. A mediation engine that implements the framework automatically detects and reconciles semantic differences at different times. We articulate that this extended COIN framework is suitable for reasoning on the Semantic Web.

Reasoning about Temporal Context using Ontology and Abductive Constraint Logic Programming

The underlying assumptions for interpreting the meaning of data often change over time, which further complicates the problem of semantic heterogeneities among autonomous data sources. As an extension to the COntext INterchange (COIN) framework, this paper introduces the notion of temporal context as a formalization of the problem. We represent temporal context as a multi-valued method in F-Logic; however, only one value is valid at any point in time, the determination of which is constrained by temporal relations. This representation is then mapped to an abductive constraint logic programming framework with temporal relations being treated as constraints. A mediation engine that implements the framework automatically detects and reconciles semantic differences at different times. We articulate that this extended COIN framework is suitable for reasoning on the Semantic Web.