LOGIQUE - LOGIC

CNRS - Université Paris 7 (Jussieu)

University of Bonn

Sylvain Poirier – This work aims to rebuild mathematics in deep, clarified and optimized ways, from model theory and a new formalization of set theory (with the formal and philosophical articulations between them), to universal algebra and tensors.

Sylvain Poirier РPrincipalement: D̩but de livre sur les fondements des math̩matiques

Development and Application of Logic Programming Tools for Knowledge Based Systems.

CEC (Coop. in Sci. and Tech. with Central and Eastern European Countries) Project 10979: 420000 ECU.

The CUBIQ project is led by Peter Szeredi of IQSOFT, a Hungarian software company with a range of interests including Prolog-based Expert Systems software products. The project is developing improved Logic Programming tools for Expert Systems, incorporating parallel processing (with Aurora/Andorra) and diagrammatic interaction.

DIG conducts research into human-computer interaction through node-and-link diagrams. Its work has mainly concerned 3D interactive diagrams and diagrams that `self-organise' to accommodate ongoing change their contents. Its interests span theory, supporting technology and applications, notably in user interfaces for knowledge-system developers and end-users.

OSHL theorem prover is based a novel first order theorem proving strategy -- ordered semantic hyper linking. Ordered semantic hyper linking (OSHL) is an instance-based refutational theorem proving strategy. It solves first order problems by reducing them to propositional problems, and it uses an efficient propositional decision procedure. It uses natural semantics of an input problem to guide its search. It also incorporates term rewriting to handle equality. The propositional efficiency, semantic guidance and equality support allow OSHL to solve problems that are difficult for many other strategies.

My prover Gandalf won this year at CASC-14, the yearly competition of classical first order automated theorem provers.

is a popular generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).

Formal Specifications and Program Validation

ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models.

A general overview of poplog, its history, how it became available free of charge, and pointers to other sites with information about poplog, etc.

Dave Rusin The mathematical Atlas

European Association for Computer Science Logic

The EACSL was founded on July 14th 1992, by computer scientists and logicians from 14 countries. The Association acts as an international professional non-profit organization.

Computer science logic is an interdisciplinary field between mathematical logic and computer science. The EACSL promotes computer science logic in the areas of scientific research and education.

ESPRIT Network of Excellence in Computational Logic.

to be held in Hamburg, Germany on August 4-15, 2008.

Since the first conference held in Marseilles in 1982, ICLP has been the

to be held in Hamburg, Germany on August 4-15, 2008.

Articles et Cours en ligne

OSHL

Peter Dybjer, Thierry Coquand, Henrik Persson, Jan Smith, Makoto Takeyama, Catarina Coquand, Ilya Beylin

Foundations of Mathematics Logic and Mathematics , Partial Realizations of Hilbert's Program , two courses Foundations of Mathematics I, Foundations of Mathematics II

Stanford Encyclopedia of Philosophy

Stanford Encyclopedia of Philosophy

Directory with code from the Gazdar & Mellish books. Also included in the contrib tarball.

E is a a purely equational theorem prover for full first-order logic

family of automated theorem provers

Written and maintained by Tanel Tammet

Gandalf is a family of theorem provers, currently including versions for classical 1-st order logic, intuitionistic 1-st order logic, propositional linear logic and a subset of Martin Löf's type theory. At the moment only the classical 1-st order version is distributed on the net.

This describes the available versions of poplog and the optional extras, all of which can be fetched free of charge. They are all provided as gzipped tar files (tarballs).

A half-serious demonstration of story grammars using the same grammar library.

If you wish to develop a package with a graphical front end you may also find the RCLIB extension useful

is developed at the University of Bern in Switzerland.

The LWB offers the possibility to work in a user-friendly way in classical and non-classical propositional logics, including nonmonotonic approaches.

There are several groups of functions: functions concerning provability simplification of formulas computation of normal forms embeddings, generation of random formulas, ...

is a popular generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).

est un outil de vérification de programmes.

Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine.

Ergo is an automatic theorem prover dedicated to program verification.

Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions.

is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

is a SMT (Satisfiability Modulo Theories) prover. There are presently two branches of haRVey: haRVey-SAT and haRVey-FOL.

HOL 4 is the latest version of the HOL automated proof system for higher order logic: a programming environment in which theorems can be proved and proof tools implemented.

The CTAN macros/latex/contrib/karnaugh/ directory

Karnaugh maps and Veitch charts are used to simplify logic equations.

Computes the theorems of the PQ system from the book Godel Escher Bach. formal.tgz

Jean-Paul Davalan

University of Toronto - Stephen Cook

Mathematical Logic, Foundations of Mathematics I ...

Jean Gallier Revised on-line version (2003)

many other texts

Jean-Yves Girard Cours de théorie de la démonstration, Roma Tre, Octobre-Décembre 2004.

The Blind Spot Lectures on proof-theory, Roma Tre, October-December 2004. English translation.

Par Patrick Dehornoy [d'après Woodin]

Séminaire Bourbaki Mars 2003 55ème année, 2002-2003, no 915

W. Hugh Woodin

Bjorn Poonen

x3 + y3 + z3 = 33? This is an unsolved problem.

Gregory J. Chaitin, chaitin@watson.ibm.com Bulletin of the European Association for Theoretical Computer Science (EATCS), No. 50 (June 1993), pp. 314-328

Lecture donnée le jeudi 22 octobre 1992 à l'occasion d'un colloque sur les Mathématiques et l'Informatique tenu à l'Université de New Mexico. La lecture a été enregistrée sur vidéo et le texte suivant est une transcription de l'enregistrement.

by Karlis Podnieks

maintained at Los Alamos

proves rigorously from first principles the major propositions of elementary

J-P. RESSAYRE (paru en TCS 257 (2001))(page web)

[d'après Ehud Hrushovski] Text of a conference at the Bourbaki Seminar Volume 1999-2000, Exposé 870, Mars 2000 Elisabeth Bouscaren (Jussieu)

nstitute for Logic at the University of Vienna

Review of Automated Development of Fundamental Mathematical Theories by Art Quaife

NEWSLETTER No. 38, December 1997

(Subscription)

Jean-Yves Girard - Luminy CNRS - 5 avril 2005 - Textes en français

1 Existence contre essence 2 Le théorème d'incomplétude 3 Le calcul (classique) des séquents LK 4 Les systèmes intuitionnistes LJ et NJ 5 Interprétations fonctionnelles 6 Le système F 7 L'interprétation catégorique. 8 Espaces cohérents. 9 La logique linéaire 10 Perfection contre imperfection 11 Réseaux de démonstration. 12 Une hypothèse : la polarisation 13 La ludique : desseins 14 La ludique : comportements. 15 Ludique : la reconstruction. 16 Les exponentielles, orthodoxes ou non... 17 Espaces cohérents quantiques 18 Encore des réseaux ! 19 L'équation de rétroaction. 20 Géométrie de l'interaction hyperfinie

Ce petit cours de logique s'adresse a priori aussi bien aux mathématiciens qu'aux informaticiens, aux physiciens qu'aux philosophes et aux linguistes ; et, comme nous ne sommes plus au XVIème , ni même au XVIIIème , siècle, il est bien évidemment voué à l'échec...

Elisabeth Bouscaren Équipe de Logique Mathématique Jussieu

Notes complémentaires. Exercices et exemples. Partiels. Devoirs

Frank Pfenning

REM d'Orléans Groupe liaison lycée post-bac

Dr Larry Paulson

Frank Pfenning

Jean Goubault-Larrecq Le 02 août 1999

A tutorial introduction to poprulebase, explaining a subset of its features.

A more complete overview of poprulebase (needs to be complemented by other files in the same directory)

Shows how to combine symbolic condition-action rules with "sub-symbolic" mechanisms (e.g. neural nets) in a hybrid system.

M. Randall Holmes and J. Alves-Foss

by Geoff Sutcliffe and Christian Suttner

Gottlob Frege (b. 1848, d. 1925) was a German mathematician, logician, and philosopher who worked at the University of Jena. Frege essentially recreated the discipline of logic by constructing the first `predicate calculus'.

Frege's Logic, Theorem, and Foundations for Arithmetic

Created by Sylvain Poirier – Here is a list of research groups and departments (and some isolated logics specialists in other departments) in the foundations of mathematics and computer science (logic, set theory, model theory, theoretical computer science, proof theory, programming languages).