On Multiset Ordering

• Autorzy: Grzegorz Bancerek
• Języki publikacji: EN

Abstrakty

EN

Formalization of a part of [11]. Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists x ∈ M1 such that M1(x) > N1(x) and (∀y ∈ N1)x ⊀ y. It should be M1(x) ⩾ N1(x). Nevertheless we do not know whether x ∈ N1 or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].

Słowa kluczowe

EN

ordering; Dershowitz-Manna ordering

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 06F05: Ordered semigroups and monoids

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2016
• Tom: 24
• Numer: 2
• Strony: 95-106

Daty

wydano

2016-06-01

otrzymano

2015-12-31

online

2016-12-08

Twórcy

autor

Grzegorz Bancerek

• Association of Mizar Users, Białystok,

Identyfikatory

DOI

10.1515/forma-2016-0008