An investigation of the laws of thought, on which are founded the mathematical theories of logic and probabilities.

Mode of access: Internet.

An investigation of the laws of thought, on which are founded mathematical theories of logic and probabilities.

Mode of access: Internet.

A comparative discussion of variable-valued logic and grammatical inference /

Bibliography: p. 45-46.

Probability and the logic of rational belief.

Includes bibliography.

Symbolic logic,

"Index of bibliographical references": p. [439]-443.

An introduction to modern logic; an elementary textbook of symbolic logic.

Mode of access: Internet.

Mathematics and logic for digital devices.

Mode of access: Internet.

A decision method for elementary algebra and geometry

"This report...was written while the project was a part of Douglas Aircraft Co., inc."

A primer of logic,

Mode of access: Internet.

Correcció d'exercicis de lògica per l'ACME

La Universitat de Girona, i més concretament el Departament d’Informàtica i Matemàtica Aplicada, ja fa uns anys que ha posat en marxa el Projecte Avaluació Continuada i Millora de l’Ensenyament, també anomenat ACME. Aquest projecte és una plataforma d'e-learning, és a dir, un sistema d’aprenentatge a través de la xarxa que potencia la col•laboració digital i el bescanvi d’informació entre alumne i professor. El creixement que ha experimentat la plataforma, ha estat possible gràcies al disseny modular de l’aplicació, on cada nova funcionalitat que estava essent desenvolupada evolucionava de manera independent a la resta de la plataforma i sense comprometre’n el funcionament. Per afegir un nou mòdul a l’ACME, s’utilitzen els mòduls de base que confereixen l'estructura a la plataforma i les eines per incorporar nous mòduls, amb el que la implantació d’aquests a la plataforma és d’elevada senzillesa. Actualment, la majoria de les assignatures de primer del Grau d’Informàtica ja disposen d’exercicis adaptats a la plataforma, el que dóna una uniformitat en les eines i plataformes que utilitzen els alumnes en la seva formació. Però no hi són totes les assignatures, falta incloure l’assignatura de Lògica a la plataforma. D’aquesta manera, tant els alumnes com els professors de l’assignatura, podran treure profit dels beneficis esmentats que aporta l’ACME. Concretament, a l’assignatura de Lògica es disposava d’uns aplicatius a la plataforma Moodle de la Universitat de Girona on es guiava a l’alumne en la resolució dels exercicis. Aquest mètode és molt interessant com a mètode pedagògic per a l’aprenentatge inicial de l’assignatura, però no representa un repte real on els alumnes hagin d’aplicar els seus coneixements per a la seva realització. Els alumnes també disposaven d’un dossier on se’ls proposava uns exercicis molt complets, i a les pàgines finals d’aquest se’ls donava la solució. Aleshores, de manera voluntària els alumnes realitzaven els exercicis i comprovaven amb la solució si havien aprés a resoldre’ls. Per tant, tant els responsables de l'assignatura de Lògica com els responsables de la plataforma ACME van veure que es podrien desenvolupar eines a l'ACME per tal de corregir de forma automàtica els exercicis de l'assignatura. Incorporar l’assignatura de Lògica a l’ACME permet que els alumnes es vegin més involucrats a fer exercicis durant els curs de manera continuada, gràcies als terminis d’entrega, i facilita als professors la seva tasca deslliurant-los de les correccions i oferint-los-hi eines de seguiment

A Variant of Higher-Order Anti-Unification

We present a rule-based Huet’s style anti-unification algorithm for simply-typed lambda-terms in ɳ long β normal form, which computes a least general higher-order pattern generalization. For a pair of arbitrary terms of the same type, such a generalization always exists and is unique modulo α equivalence and variable renaming. The algorithm computes it in cubic time within linear space. It has been implemented and the code is freely available

An Efficient Nominal Unification Algorithm

Nominal Unification is an extension of first-order unification where terms can contain binders and unification is performed modulo α equivalence. Here we prove that the existence of nominal unifiers can be decided in quadratic time. First, we linearly-reduce nominal unification problems to a sequence of freshness and equalities between atoms, modulo a permutation, using ideas as Paterson and Wegman for first-order unification. Second, we prove that solvability of these reduced problems may be checked in quadràtic time. Finally, we point out how using ideas of Brown and Tarjan for unbalanced merging, we could solve these reduced problems more efficiently

A Write-Based Solver for SAT Modulo the Theory of Arrays

The extensional theory of arrays is one of the most important ones for applications of SAT Modulo Theories (SMT) to hardware and software verification. Here we present a new T-solver for arrays in the context of the DPLL(T) approach to SMT. The main characteristics of our solver are: (i) no translation of writes into reads is needed, (ii) there is no axiom instantiation, and (iii) the T-solver interacts with the Boolean engine by asking to split on equality literals between indices. As far as we know, this is the first accurate description of an array solver integrated in a state-of-the-art SMT solver and, unlike most state-of-the-art solvers, it is not based on a lazy instantiation of the array axioms. Moreover, it is very competitive in practice, specially on problems that require heavy reasoning on array literals

Teoria de conjuntos fuzzy e aplicações

Pós-graduação em Matemática Universitária - IGCE