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.

Bank of Canada Records, 1958-1989

The Bank of Canada first introduced Canada Savings Bonds during the First and Second World Wars. At the time, they were known as War Savings Certificates and Victory Bonds and were used to fund the war effort. In 1946, Canada Savings Bonds were used as part of Canada’s Postwar Financing Program. At that time, the government also introduced the sale of bonds through payroll deduction. Canada Savings Bonds proved to be very popular, providing investors with a convenient, flexible and safe investment. Over time the bonds failed to remain competitive with other low-risk investment options, and the high cost of administering the program called into question its relevance. An independent report commissioned by the government in 2004 recommended that the bonds be phased out, however, the government decided to keep the program and make some revisions. As of 2012, Canada Savings Bonds are available exclusively through the payroll savings program, while Canada Premium Bonds (introduced in 1998) are available through financial institutions, dealers and by phone.

L’analogie juridique dans la Critique de la raison pure

La Critique de la raison pure est traversée de part en part par une analogie juridique dont l’étude peut enrichir la compréhension de l’œuvre. Il est ainsi question, dès la préface, d’une raison qui se juge elle-même devant son propre tribunal, ce qui constituera le point de départ de notre analyse. Or, ce tribunal très particulier doit se fonder sur une connaissance de soi approfondie de la raison. Cette entreprise est de fait réalisée au fil des développements de la Critique. Le rôle bien particulier joué à cet égard par les trois déductions présentes dans l’œuvre sera dûment examiné. On verra par ailleurs que la déduction doit elle-même être considérée plutôt comme procédure d’inspiration juridique que comme inférence, tout en conservant pourtant un statut de preuve philosophique. Les nombreuses allusions juridiques effectuées par Kant au fil de l’œuvre seront ainsi mises à profit dans le cadre de cette interprétation.

Perceptions du «bien manger» chez des intervenants clés agissant auprès d’enfants fréquentant des services de garde préscolaires

Contexte : La petite enfance constitue une période importante dans l’acquisition de saines habitudes alimentaires. Par leurs connaissances, attitudes, croyances, pratiques et perceptions en alimentation et nutrition, plusieurs intervenants influencent les jeunes enfants : parents, responsables de l’alimentation et éducatrices en services de garde. Objectifs : Cette étude décrit et analyse les perceptions du « bien manger » de 113 responsables de l’alimentation, de 302 éducatrices et de 709 parents d’enfants âgés de 2 à 5 ans en services de garde au Québec. Méthodologie : Ce mémoire porte sur une question ouverte, répétée dans trois questionnaires autoadministrés de la recherche Offres et pratiques alimentaires revues dans les services de garde au Québec. Les réponses ont été recueillies de 2009 à 2010 et analysées au moyen d’une grille de codification construite de manières déductive et inductive. Résultats : L’analyse des données recueillies montre la récurrence des thèmes de la variété, l’équilibre, la modération, des légumes et fruits, mais aussi l’émergence du plaisir, de la santé, du GAC, des qualités organoleptiques, des pratiques coercitives et de la commensalité. Cette recherche dévoile que la variété, la santé et l’équilibre sont communs aux trois catégories d’intervenants, alors que le GAC, le plaisir, la saine alimentation et les qualités organoleptiques figurent plutôt dans les perceptions d’intervenants spécifiques. Conclusion : Ce portrait illustre la compréhension du « bien manger » qu’ont des intervenants jouant un rôle important dans le développement d’enfants âgés de 2 à 5 ans. En outre, il permet d’éclairer les acteurs développant messages, interventions et politiques de santé publique faisant la promotion de la saine alimentation et favorisant la mise en place d’environnements appuyant l’adoption de saines habitudes alimentaires dans les services de garde du Québec ainsi que dans les ménages.

ONTIC: A Knowledge Representation System for Mathematics

Ontic is an interactive system for developing and verifying mathematics. Ontic's verification mechanism is capable of automatically finding and applying information from a library containing hundreds of mathematical facts. Starting with only the axioms of Zermelo-Fraenkel set theory, the Ontic system has been used to build a data base of definitions and lemmas leading to a proof of the Stone representation theorem for Boolean lattices. The Ontic system has been used to explore issues in knowledge representation, automated deduction, and the automatic use of large data bases.

Procedures as a Representation for Data in a Computer Program for Understanding Natural Language

This paper describes a system for the computer understanding of English. The system answers questions, executes commands, and accepts information in normal English dialog. It uses semantic information and context to understand discourse and to disambiguate sentences. It combines a complete syntactic analysis of each sentence with a "heuristic understander" which uses different kinds of information about a sentence, other parts of the discourse, and general information about the world in deciding what the sentence means. It is based on the belief that a computer cannot deal reasonably with language unless it can "understand" the subject it is discussing. The program is given a detailed model of the knowledge needed by a simple robot having only a hand and an eye. We can give it instructions to manipulate toy objects, interrogate it about the scene, and give it information it will use in deduction. In addition to knowing the properties of toy objects, the program has a simple model of its own mentality. It can remember and discuss its plans and actions as well as carry them out. It enters into a dialog with a person, responding to English sentences with actions and English replies, and asking for clarification when its heuristic programs cannot understand a sentence through use of context and physical knowledge.

Un análisis de la relación comercial entre Colombia y Estados Unidos en el marco de los acuerdos comerciales

Estados Unidos es el principal socio comercial de Colombia: es el país de destino del 36% de las exportaciones colombianas y el país de origen del 25% de las importaciones colombianas (DANE, 2011). La relación entre ambos profundizó sus lazos con el programa arancelario ATPA, luego ATPDEA, en virtud del cual al 80% de la oferta exportable de Colombia se le ofrecía ya sea con libre acceso al mercado estadounidense, o entrada con pago de arancel reducido. Posteriormente, la entrada en vigencia del TLC generó las bases para una relación comercial más profunda aún, que también incluyera beneficios para Estados Unidos y prolongara y profundizara los beneficios que Colombia ya recibía. Este trabajo se enfoca en analizar paso a paso el comportamiento del comercio entre ambos países a través de los años y, por supuesto, el comportamiento actual del comercio, teniendo siempre en cuenta el contexto económico mundial, así como el contexto económico bilateral.

Durability assessment of PbTe/II-IV infrared filters (Space Shuttle 1st LDEF)

Residual stress having been further reduced, selected infrared coatings composed of thin films of (PbTe/ ZnS (or ZnSe) can now be made which comply with the durability requirements of MIL-48616 whilst retaining transparency. Such improved durability is due to the sequence:- i) controlled deposition, followed by ii) immediate exposure to air, followed by iii) annealing in vacuo to relieve stress. (At the time of writing we assume the empiric procedure "exposure to air/annealing in vacuo" acts to relieve the inherent stresses of deposition). As part of their testing, representative sample filters prepared by the procedure are being assembled for the shuttle's 1st Long Duration Exposure Facility (to be placed in earth orbit for a considerable period and then recovered for analysis). The sample filters comprise various narrowband-designs to permit deduction of the constituent thin film optical properties. The Reading assembly also contains representative sample of the infrared crystals, glasses, thin-film absorbers and bulk absorbers, and samples of shorter-wavelength filters prepared similarly but made with Ge/SiO. Findings on durability and transparency after exposure will be reported.

Overcoming principles: dialogue in business ethics

Basing itself upon a virtue-ethics approach, this paper questions the value of syllogistic or deductive approaches to teaching business ethics and to the modelling of the kinds of judgments that executives are asked to make in situations of moral complexity. It urges that the teaching of ethical theories, of ethical principles, and of logical methods of moral thinking, and the use of hypothetical or historical scenarios, be augmented by the method of `Real Case Dialogue' which more nearly models the eal and intense existential realities of ethical decision making. A brief description of such a dialogue is offered so aslo provide an example.

The tax treatment of employee stock options : generous to a fault

In the 2000 budgets, both the federal and Ontario governments introduced changes to the tax treatment of employee stock options for the explicit purpose of making their tax treatment in Canada similar to or more favourable than that in the United States. The federal budget added a deferral, similar to that currently applicable to options granted by Canadian-controlled private corporations, for up to $100,000 per year of public company stock options. The Ontario budget introduced an exemption from tax for employees involved in research and development on the first $100,000 per year of employee benefits arising on the exercise of qualified stock options or on eligible capital gains arising from the sale of shares acquired by the exercise of eligible stock options. These proposals reflect the apparent acceptance by the two governments that there is a “brain drain” from Canada to the United States of knowledge workers in the “new” economy and that reductions in Canadian taxes should stem this drain. In the author’s view, the tax treatment of employee stock options, even without these changes, is overly generous. Both the federal and provincial proposals ignore the fact that most employee stock options are taxed more favourably in Canada than in the United States in any event. In particular, most employee stock option benefits in Canada are taxed at capital gains tax rates, whereas in the United States most are taxed at full rates. While the US Internal Revenue Code does provide capital gains tax treatment for certain employee stock option benefits, a number of preconditions must be met. Most important, the shares acquired pursuant to the options must be held for a minimum of one year after the option is exercised. In addition, there are monetary limits on the amount of options that qualify for capital gains treatment. In Canada, there are generally no holding period requirements or monetary limits that apply in order for the option holder to benefit from capital gains tax rates. Empirical evidence indicates that the vast majority of employees in the United States exercise their options and immediately sell the shares acquired. These “cashless exercises” do not benefit from capital gains treatment in the United States, whereas similar cashless exercises in Canada generally do. This empirical evidence suggests not only that the 2000 budget proposals are unwarranted, but also that the existing treatment of employee stock options in Canada is already more generous than that in the United States. This article begins with a theoretical “benchmark” for the taxation of employee stock options. The author suggests that employee stock options should be treated in the same manner as other income from employment. In theory, the value of the benefit should be included in income when the option is granted or vests. However, owing to the practical difficulty of valuing employee stock options, the theoretical benchmark proposed is that the value of the benefit (the difference between the fair market value of the shares acquired and the strike price under the option) be taxed when the shares are acquired, and the employer be entitled to a corresponding deduction. The employee stock option rules in Canada and the United States are then compared and contrasted with each other and the benchmark treatment. The article then examines the arguments that have been made for favourable treatment of employee stock options. Included in this critique is a review of the recent empirical work on the Canadian brain drain. Empirical studies suggest that the brain drain—if it exists at all—is small and that, despite what many newspapers and right-wing think-tanks would have us believe, lower taxes in the United States are not the cause. One study, concluding that taxes do have an effect on migration, suggests that even if Canada adopted a tax system identical to that in the United States, the brain drain would be reduced by a mere 10 percent. Indeed, even if Canada eliminated income tax altogether, it would not stop the brain drain. If governments here want to spend money in order to stem the brain drain, they should focus on other areas. For example, Canada produces fewer university graduates in the fields of mathematics, sciences, and engineering than any other G7 country except Italy. The short supply of university graduates in these fields, the apparent loss of top-calibre academics to US
universities, and the consequent lower levels of university research in these areas (an important spawning ground for new ideas in the “new” knowledge-based economy) suggest that Canada may be better served by devoting more resources to its university institutions, particularly in post-graduate programs, rather than continuing the current trend of budget cuts that universities have endured and may further endure if taxes are reduced.
As far as employee stock options are concerned, if Canada does want to look to the United States for guidance on tax reform (which it seems to do with increasing frequency of late), it should adopt the US rules applicable to nonstatutory options, which are close to the proposed benchmark treatment. In the absence of preferential tax treatment, employee stock options would still be included in compensation packages provided that there were sound business reasons for their use. No persuasive evidence has been put forward that the use of stock options, in the absence of tax incentives, is suboptimal. Indeed, the US experience suggests quite the opposite.

Monodic Temporal Resolution

First-order temporal logic is a coincise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics have identified important enumerable and even decidable fragments. In this paper we present the first resolution-based calculus for monodic first-order temporal logic. Although the main focus of the paper is on establishing completeness result, we also consider implementation issues and define a basic loop-search algorithm that may be used to guide the temporal resolution system.

Kanger's Choices in Automated Reasoning

This article explains these choices and their place in modern automated deduction.

Evidence Algorithm and Processing Formalized Mathematical Texts

The goal of a research programme Evidence Algorithm is a development of an open system of automated proving that is able to accumulate mathematical knowledge and to prove theorems in a context of a self-contained mathematical text. By now, the first version of such a system called a System for Automated Deduction, SAD, is implemented in software. The system SAD possesses the following main features: mathematical texts are formalized using a specific formal language that is close to a natural language of mathematical publications; a proof search is based on special sequent-type calculi formalizing natural reasoning style, such as application of definitions and auxiliary propositions. These calculi also admit a separation of equality handling from deduction that gives an opportunity to integrate logical reasoning with symbolic calculation.

Electronic waste exchange for just-in-time building demolition

Waste exchange is as a facilitator for construction and demolition waste deduction by reuse and recycling in construction projects. The just-in-time philosophy, which has been well cultivated in the manufacturing industry, is highly adoptable for demolition projects. Particularly, waste exchange that is usually performed after the actual demolition process can be shifted forward so that waste inventory from demolition is eliminated or reduced to facilitate waste reuse and recycling. A web-based waste exchange system is an ideal platform to enable communications among project participants before a demolition project commences so that waste materials can be sold before they are produced. Therefore, the productivity of the demolition project could be improved. This research paper aims to investigate and analyse the adoption of just-in-time philosophy in building demolition project management. It also describes the development of the proposed web-based waste exchange system that implements just-in-time demolition in detail, including its functionalities, information flows and major components.

Spatial reasoning via active observation

This paper presents a model for space in which an autonomous agent acquires information about its environment. The agent uses a predefined exploration strategy to build a map allowing it to navigate and deduce relationships between points in space. The shapes of objects in the environment are represented qualitatively. This shape information is deduced from the agent's motion. Normally, in a qualitative model, directional information degrades under transitive deduction. By reasoning about the shape of the environment, the agent can match visual events to points on the objects. This strengthens the model by allowing further relationships to be deduced. In particular, points that are separated by long distances, or complex surfaces, can be related by line-of-sight. These relationships are deduced without incorporating any metric information into the model. Examples are given to demonstrate the use of the model.