On equivalents of well-foundedness. An experiment in MIZAR
From MaRDI portal
Publication:1961913
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
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
