One implementation of PL prover algorithm
Optimal learning systems
Preliminaries to Classical First Order Model Theory
First of a series of articles laying down the bases for classical first order model theory. These articles introduce a framework for treating arbitrary languages with equality. This framework is kept as generic and modular as possible: both the language and the derivation rule are introduced as a type, rather than a fixed functor; definitions and results regarding syntax, semantics, interpretations and sequent derivation rules, respectively, are confined to separate articles, to mark out the hierarchy...
Probabilistic verification of proofs.
Problém obecného pojetí metody GUHA
Propositional calculus proving methods in Prolog
Quelques remarques sur la complexité des algorithmes
Realizations of Loops and Groups defined by short identities
In a recent paper, those quasigroup identities involving at most three variables and of “length” six which force the quasigroup to be a loop or group have been enumerated by computer. We separate these identities into subsets according to what classes of loops they define and also provide humanly-comprehensible proofs for most of the computer-generated results.
Recherche à voisinage variable de graphes extrémaux 13. A propos de la maille
Le système AutoGraphiX (AGX1 et AGX2) permet, parmi d’autres fonctions, la génération automatique de conjectures en théorie des graphes et, dans une version plus récente, la preuve automatique de conjectures simples. Afin d’illustrer ces fonctions et le type de résultats obtenus, nous étudions systématiquement ici des conjectures obtenues par ce système et de la forme où désigne la maille (ou longueur du plus petit cycle) du graphe , un autre invariant choisi parmi le nombre de stabilité,...
Recherche à voisinage variable de graphes extrémaux 13. à propos de la maille*
Le système AutoGraphiX (AGX1 et AGX2) permet, parmi d'autres fonctions, la génération automatique de conjectures en théorie des graphes et, dans une version plus récente, la preuve automatique de conjectures simples. Afin d'illustrer ces fonctions et le type de résultats obtenus, nous étudions systématiquement ici des conjectures obtenues par ce système et de la forme où g désigne la maille (ou longueur du plus petit cycle) du graphe G=(V, E), i un autre invariant choisi parmi le nombre...
Refinements of inductive inference by Popperian and reliable machines
Restricted ideals and the groupability property. Tools for temporal reasoning
In the field of automatic proving, the study of the sets of prime implicants or implicates of a formula has proven to be very important. If we focus on non-classical logics and, in particular, on temporal logics, such study is useful even if it is restricted to the set of unitary implicants/implicates [P. Cordero, M. Enciso, and I. de Guzmán: Structure theorems for closed sets of implicates/implicants in temporal logic. (Lecture Notes in Artificial Intelligence 1695.) Springer–Verlag, Berlin 1999]....
Right division in Moufang loops
If is a group, and the operation is defined by then by direct verification is a quasigroup which satisfies the identity . Conversely, if one starts with a quasigroup satisfying the latter identity the group can be constructed, so that in effect is determined by its right division operation. Here the analogous situation is examined for a Moufang loop. Subtleties arise which are not present in the group case since there is a choice of defining identities and the identities produced by...
Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem
Fifth of a series of articles laying down the bases for classical first order model theory. This paper presents multiple themes: first it introduces sequents, rules and sets of rules for a first order language L as L-dependent types. Then defines derivability and provability according to a set of rules, and gives several technical lemmas binding all those concepts. Following that, it introduces a fixed set D of derivation rules, and proceeds to convert them to Mizar functorial cluster registrations...
Set arithmetic and the enclosing problem in dynamics
We study the enclosing problem for discrete and continuous dynamical systems in the context of computer assisted proofs. We review and compare the existing methods and emphasize the importance of developing a suitable set arithmetic for efficient algorithms solving the enclosing problem.
Some Heuristics in Automatic Theorem Proving
Some heuristics in automatic theorem proving.
Some key research problems in automated theorem proving for hardware and software verification.
This paper sketches the state of the art in the application of mechanical theorem provers to the verification of commercial computer hardware and software. While the paper focuses on the theorem proving system ACL2, developed by the two authors, it references much related work in formal methods. The paper is intended to satisfy the curiosity of readers interested in logic and artificial intelligence as to the role of mechanized theorem proving in hardware and software design today. In addition,...
Some Properties of p -Groups and Commutative p -Groups
This article describes some properties of p-groups and some properties of commutative p-groups.
Statistical approach to proof theory