All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Page 1 Next

Displaying 1 – 20 of 118

Showing per page

A graphical representation of relational formulae with complementation

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

A graphical representation of relational formulae with complementation∗

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

A Model of Mizar Concepts - Unification

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.

A proximity based macro stress testing framework

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

A reduction-based theorem prover for 3-valued logic.

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

Antiassociative groupoids

Milton Braitt, David Hobby, Donald Silberger (2017)

Mathematica Bohemica

Given a groupoid 〈 G , ☆ 〉 , and k ≥ 3 , we say that G is antiassociative if an only if for all x 1 , x 2 , x 3 ∈ G , ( x 1 ☆ x 2 ) ☆ x 3 and x 1 ☆ ( x 2 ☆ x 3 ) are never equal. Generalizing this, 〈 G , ☆ 〉 is k -antiassociative if and only if for all x 1 , x 2 , ... , x k ∈ G , any two distinct expressions made by putting parentheses in x 1 ☆ x 2 ☆ x 3 ☆ ⋯ ☆ x k are never equal. We prove that for every k ≥ 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.

Aperiodicity of the Hamiltonian flow in the Thomas-Fermi potential.

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.

Cayley's Theorem

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.

Classification results in quasigroup and loop theory via a combination of automated reasoning tools

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

Cocktail: a tool for deriving correct programs.

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

Currently displaying 1 – 20 of 118

Page 1 Next