### A deductive calculus for conditional equational systems with built-in predicates as premises.

Skip to main content (access key 's'),
Skip to navigation (access key 'n'),
Accessibility information (access key '0')

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...

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...

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.

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...

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...

Given a groupoid $\langle G,\u2606\rangle $, and $k\ge 3$, we say that $G$ is antiassociative if an only if for all ${x}_{1},{x}_{2},{x}_{3}\in G$, $({x}_{1}\u2606{x}_{2})\u2606{x}_{3}$ and ${x}_{1}\u2606({x}_{2}\u2606{x}_{3})$ are never equal. Generalizing this, $\langle G,\u2606\rangle $ is $k$-antiassociative if and only if for all ${x}_{1},{x}_{2},...,{x}_{k}\in G$, any two distinct expressions made by putting parentheses in ${x}_{1}\u2606{x}_{2}\u2606{x}_{3}\u2606\cdots \u2606{x}_{k}$ are never equal. We prove that for every $k\ge 3$, there exist finite groupoids that are $k$-antiassociative. We then generalize this, investigating when other pairs of groupoid terms can be made never equal.

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.

A formalization of the first proof from [6].

The article formalizes the Cayley's theorem saying that every group G is isomorphic to a subgroup of the symmetric group on G.

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 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....