A deductive calculus for conditional equational systems with built-in predicates as premises.
Page 1 Next
Ayala-Rincón, Mauricio (1997)
Revista Colombiana de Matemáticas
Domenico Cantone, Andrea Formisano, Marianna Nicolosi Asmundo, Eugenio Giovanni Omodeo (2012)
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
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...
Domenico Cantone, Andrea Formisano, Marianna Nicolosi Asmundo, Eugenio Giovanni Omodeo (2012)
RAIRO - Theoretical Informatics and Applications
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...
Grzegorz Bancerek (2010)
Formalized Mathematics
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.
Irène Guessarian (1988)
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
Ivan Kramosil (1975)
Kybernetika
Boris Waelchli (2016)
Dependence Modeling
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...
Gabriel Aguilera Venegas, Inmaculada Pérez de Guzmán, Manuel Ojeda Aciego (1997)
Mathware and Soft Computing
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...
Havel, Ivan M., Ivan Kramosil (1978)
Kybernetika
Khotomski, Petar Z. (1983)
Publications de l'Institut Mathématique. Nouvelle Série
Milton Braitt, David Hobby, Donald Silberger (2017)
Mathematica Bohemica
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.
Charles L. Fefferman, Luis A. Seco (1993)
Revista Matemática Iberoamericana
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.
Freek Wiedijk (2007)
Formalized Mathematics
A formalization of the first proof from [6].
Jan Štěpán (1991)
Acta Universitatis Palackianae Olomucensis. Facultas Rerum Naturalium. Mathematica
Petr Hájek (1973)
Kybernetika
Petr Hájek (1973)
Kybernetika
Petr Hájek (1974)
Kybernetika
Artur Korniłowicz (2011)
Formalized Mathematics
The article formalizes the Cayley's theorem saying that every group G is isomorphic to a subgroup of the symmetric group on G.
Volker Sorge, Simon Colton, Roy McCasland, Andreas Meier (2008)
Commentationes Mathematicae Universitatis Carolinae
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...
Michael Franssen, Harrie De Swart (2004)
RACSAM
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....
Page 1 Next