Displaying similar documents to “Abstract Reduction Systems and Idea of Knuth-Bendix Completion Algorithm”

Quasi-sums in several variables.

Maksa, Gyula, Nizsalóczki, Enikő (2006)

Acta Mathematica Academiae Paedagogicae Nyí regyháziensis. New Series [electronic only]

Similarity:

Semantics of MML Query

Grzegorz Bancerek (2012)

Formalized Mathematics

Similarity:

In the paper the semantics of MML Query queries is given. The formalization is done according to [4]

Bertrand’s Ballot Theorem

Karol Pąk (2014)

Formalized Mathematics

Similarity:

In this article we formalize the Bertrand’s Ballot Theorem based on [17]. Suppose that in an election we have two candidates: A that receives n votes and B that receives k votes, and additionally n ≥ k. Then this theorem states that the probability of the situation where A maintains more votes than B throughout the counting of the ballots is equal to (n − k)/(n + k). This theorem is item #30 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. ...

Model Checking. Part III

Kazuhisa Ishida, Yasunari Shidama (2008)

Formalized Mathematics

Similarity:

This text includes verification of the basic algorithm in Simple On-the-fly Automatic Verification of Linear Temporal Logic (LTL). LTL formula can be transformed to Buchi automaton, and this transforming algorithm is mainly used at Simple On-the-fly Automatic Verification. In this article, we verified the transforming algorithm itself. At first, we prepared some definitions and operations for transforming. And then, we defined the Buchi automaton and verified the transforming algorithm.MML...

Pairwise monotonically normal spaces

Josefa Marín, Salvador Romaguera (1991)

Commentationes Mathematicae Universitatis Carolinae

Similarity:

We introduce and study the notion of pairwise monotonically normal space as a bitopological extension of the monotonically normal spaces of Heath, Lutzer and Zenor. In particular, we characterize those spaces by using a mixed condition of insertion and extension of real-valued functions. This result generalizes, at the same time improves, a well-known theorem of Heath, Lutzer and Zenor. We also obtain some solutions to the quasi-metrization problem in terms of the pairwise monotone normality. ...