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.

Registered Nurses' Perceptions about Facilitators and Barriers to Maternal Skin to Skin Contact in the Operating Room

Abstract It is recommended that all new mothers experience skin-to-skin contact (SSC) with their newborns immediately after birth. However, SSC is not commonly practiced after cesarean deliveries. To understand facilitators and barriers regarding SSC in the operating room (OR), a descriptive online and paper survey was conducted with 68 Registered Nurses from four hospitals in Ontario. The theory of planned behavior framed the study. Nurses had positive attitudes, and believed most health care team members supported SSC in the OR, but were uncertain about their control over the behavior. Nurses who had practiced the behavior in the past had more positive attitudinal and normative beliefs, and perceived some barriers as less difficult. Attitude and past behavior were the only significant multivariate predictors of intention to practice SSC in the future. Results suggest that shifting attitude and supporting more experience with the practice may increase nurses’ implementation of SSC in the OR.

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.

L’analyse de l’introduction du changement dans les systèmes de santé des pays en développement : le cas d’un système de surveillance épidémiologique en Haïti

Les systèmes de santé des pays en développement font face à de nombreux enjeux organisationnels pour améliorer l’état de santé de leur population. Au nombre de ces enjeux, il est fréquemment mentionné la présence d’organisations internationales ayant des objectifs et caractéristiques peu convergents et qui interviennent de façon non nécessairement coordonnée. Cette thèse explore la thématique de l’introduction du changement dans ces systèmes de santé en mettant un accent spécifique sur l’enjeu lié à la présence de ces organisations internationales. La méthodologie utilisée est une analyse de concept. Cette approche méthodologique consiste à effectuer des revues critiques de la littérature sur des concepts, à mobiliser de nouvelles approches théoriques pour clarifier ces concepts et à réaliser des études de cas pour leur mise à l’épreuve empirique. En nous appuyant sur la théorie de l’action sociale de Parsons, la théorie de la complexité ainsi que les expériences d’introduction du changement dans différents systèmes de santé, nous avons développé un cadre théorique d’analyse de l’introduction du changement dans les systèmes de santé des pays en développement (1er concept). Ce cadre théorique, qui suggère de concevoir le processus d’introduction du changement comme un système d’action sociale complexe et émergent, a été appliqué à l’analyse de l’introduction d’un système de surveillance épidémiologique en Haïti. Plus précisément, nous avons analysé une étape ainsi que certains aspects du mécanisme sous-jacent au processus d’introduction du changement. Ce faisant, nous avons analysé, dans les deux premiers articles de la thèse, l’étape d’adoption du système de surveillance épidémiologique (2ème concept) ainsi que les déterminants de la collaboration entre les organisations impliquées dans le processus d’introduction du changement (3ème concept). Les résultats de ces analyses nous ont permis d’objectiver de faibles niveaux d’adoption, ainsi qu’une faible articulation des déterminants de la collaboration entre les différentes organisations impliquées dans le processus d’introduction du changement. Partant de ces constats, nous avons pu mettre en évidence, dans le troisième article, une phase de « chaos » dans le fonctionnement du système de santé d’Haïti. Cette phase de « chaos », qui pourrait expliquer les difficultés liées à l’introduction du changement dans les systèmes de santé des pays en développement en général et plus particulièrement en Haïti, était caractérisée par la présence d’un ordre sous-jacent au désordre apparent dans le fonctionnement de certaines composantes du système de santé d’Haïti, l’existence d’une instabilité, d’une imprédictibilité ainsi que d’une invariance structurelle aux différents niveaux de gouvernance. Par ailleurs, cette recherche a également permis de démontrer que les caractéristiques du « chaos » sont entretenues par la présence de trois groupes de systèmes d’action sociale bien articulés et bien cohérents à tous les échelons de la pyramide sanitaire en Haïti. Il s’agissait des systèmes d’action liés aux agences de coopération bilatérale, ceux liés aux initiatives ou fondations internationales de lutte contre le sida et finalement ceux associés aux organisations onusiennes. Ces systèmes d’action sociale sont en outre associés à d’autres systèmes d’action plus complexes qui sont situés à l’extérieur du système de santé d’Haïti. Au regard de ces résultats, nous avons proposé une nouvelle approche permettant de mieux appréhender l’introduction du changement dans les systèmes de santé des pays en développement et qui s’inscrit dans une logique permettant de favoriser une plus grande variété et une plus grande diversification. Cette variété et cette diversification étant soutenue par la création et la mise en place de plusieurs interconnections entre tous les systèmes d’action en présence dans les systèmes de santé qu’ils soient d’appartenance nationale, internationale ou qu’ils agissent au niveau central, départemental ou local. La finalité de ce processus étant l’émergence de propriétés systémiques issues non seulement des propriétés des groupes de systèmes d’action individuels qui interviennent dans la constitution du système émergent, mais aussi d’autres propriétés résultant de leur mise en commun.

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.

Studies on the technological aspects and economic efficiency of trawl gear operating along the Cochin coast

Trawling, despite being heavily energy expensive, still continues to be the most energy expensive fishing method particularly so in View of the export oriented nature of the Indian seafood industry. This study therefore aims at analyzing the efficiency of trawls operation from Cochin, an important fishing center along the southwest coast of India. The analysis is made along two perspectives - economic and technological. Even though technological efficiency complement economic efficiency, in the fishing parlance, parameters like the size composition of the catch, selectivity factors, etc., will have a direct bearing on the technological qualities of the trawl, and which parameters will have a significant impact on the effective exploitation of a fishery stock. Whereas the technological analysis aims at improving the efficiency with regard to the effective utilization of fuel and fishery stocks, economic analysis ascertains the present status of the trawling operations from the commercial angle.

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.

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.