A deductive calculus for conditional equational systems with built-in predicates as premises.
A graphical representation of relational formulae with complementation
We study translations of dyadic first-order sentences into equalities between relational expressions. The proposed translation techniques (which work also in the converse direction) exploit a graphical representation of formulae in a hybrid of the two formalisms. A major enhancement relative to previous work is that we can cope with the relational complement construct and with the negation connective. Complementation is handled by adopting a Smullyan-like uniform notation to classify and decompose...
A graphical representation of relational formulae with complementation∗
We study translations of dyadic first-order sentences into equalities between relational expressions. The proposed translation techniques (which work also in the converse direction) exploit a graphical representation of formulae in a hybrid of the two formalisms. A major enhancement relative to previous work is that we can cope with the relational complement construct and with the negation connective. Complementation is handled by adopting a Smullyan-like...
A Model of Mizar Concepts - Unification
The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from [6] and [7]. The theory presented is an abstraction from the existing implementation of the Mizar system and is devoted to the formalization of Mizar expressions. The concepts formalized here are: standarized constructor signature, arity-rich signatures, and the unification of Mizar expressions.
A note on fixpoint techniques in data base recursive logic programs
A probabilistic approach to automaton-environment systems
A proximity based macro stress testing framework
In this a paper a non-linear macro stress testing methodology with focus on early warning is developed. The methodology builds on a variant of Random Forests and its proximity measures. It is embedded in a framework, in which naturally defined contagion and feedback effects transfer the impact of stressing a relatively small part of the observations on the whole dataset, allowing to estimate a stressed future state. It will be shown that contagion can be directly derived from the proximities while...
A reduction-based theorem prover for 3-valued logic.
We present a new prover for propositional 3-valued logics, TAS-M3, which is an extension of the TAS-D prover for classical propositional logic. TAS-M3 uses the TAS methodology and, consequently, it is a reduction-based method. Thus, its power is based on the reductions of the size of the formula executed by the F transformation. This transformation dynamically filters the information contained in the syntactic structure of the formula to avoid as much distributions as possible, in order to improve...
A stochastic approach to robot plan formation
An implementation of the induction rule into resolution procedures for automatic theorem proving.
Antiassociative groupoids
Given a groupoid , and , we say that is antiassociative if an only if for all , and are never equal. Generalizing this, is -antiassociative if and only if for all , any two distinct expressions made by putting parentheses in are never equal. We prove that for every , there exist finite groupoids that are -antiassociative. We then generalize this, investigating when other pairs of groupoid terms can be made never equal.
Aperiodicity of the Hamiltonian flow in the Thomas-Fermi potential.
In [FS1] we announced a precise asymptotic formula for the ground-state energy of a non-relativistic atom. The purpose of this paper is to establish an elementary inequality that plays a crucial role in our proof of that formula. The inequality concerns the Thomas-Fermi potentialVTF = -y(ar) / r, a > 0, where y(r) is defined as the solution of⎧ y''(x) = x-1/2y3/2(x),⎨ y(0) = 1,⎩ y(∞) = 0.
Arrow's Impossibility Theorem
A formalization of the first proof from [6].
Automated theorem proving in monadic predicate calculus
Automatic listing of important observational statements. I
Automatic listing of important observational statements. II
Automatic listing of important observational statements. III
Cayley's Theorem
The article formalizes the Cayley's theorem saying that every group G is isomorphic to a subgroup of the symmetric group on G.
Classification results in quasigroup and loop theory via a combination of automated reasoning tools
We present some novel classification results in quasigroup and loop theory. For quasigroups up to size 5 and loops up to size 7, we describe a unique property which determines the isomorphism (and in the case of loops, the isotopism) class for any example. These invariant properties were generated using a variety of automated techniques --- including machine learning and computer algebra --- which we present here. Moreover, each result has been automatically verified, again using a variety of techniques...
Cocktail: a tool for deriving correct programs.
Cocktail is a tool for deriving correct programs from their specifications. The present version is powerful enough for educational purposes. The tool yields support for many sorted first order predicate logic, formulated in a pure type system with parametric constants (CPTS), as the specification language, a simple While-language, a Hoare logic represented in the same CPTS for deriving programs from their specifications and a simple tableau based automated theorem prover for verifying proof obligations....