On equivalents of well-foundedness. An experiment in MIZAR

DOI10.1023/A:1006218513245zbMath0944.68168OpenAlexW1546740898MaRDI QIDQ1961913

Piotr Rudnicki, Andrzej Trybulec

Publication date: 27 March 2000

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1006218513245

zbMATH Keywords

well-foundednessMIZAR

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Axiomatics of classical set theory and its fragments (03E30) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04)

Related Items

Four decades of {\textsc{Mizar}}. Foreword ⋮ Mathematical method and proof ⋮ MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics ⋮ Commutative algebra in the Mizar system ⋮ MPTP 0.2: Design, implementation, and initial experiments ⋮ About quotient orders and ordering sequences ⋮ Structured derivations: a unified proof style for teaching mathematics ⋮ Computer proofs about finite and regular sets: The unifying concept of subvariance. ⋮ The Mizar Mathematical Library in OMDoc: translation and applications ⋮ Custom automations in Mizar ⋮ Formal power series ⋮ The axiomatization of propositional logic ⋮ On the Structure of Mizar Types ⋮ Adapting functional programs to higher order logic ⋮ Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking ⋮ Presenting and Explaining Mizar

Uses Software

• Mizar