Computer proofs about finite and regular sets: The unifying concept of subvariance.

DOI10.1016/S0747-7171(03)00023-3MaRDI QIDQ1404990zbMATH OpenOpenAlexFDO

Authors Johan Gijsbertus Frederik Belinfante

Publication date 25 August 2003

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0747-7171(03)00023-3

zbMATH Keywords

FiniteRegularitySubvariance

Mathematics Subject Classification ID

Recommendations

• An automated prover for Zermelo-Fraenkel set theory in Theorema
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• A formalisation of finite automata using hereditarily finite sets
• Computer theorem proving in mathematics
• scientific article; zbMATH DE number 1641581

Cites work

• scientific article; zbMATH DE number 1614691 (Why is no real title available?)
• scientific article; zbMATH DE number 42735 (Why is no real title available?)
• scientific article; zbMATH DE number 44058 (Why is no real title available?)
• scientific article; zbMATH DE number 158462 (Why is no real title available?)
• scientific article; zbMATH DE number 1314876 (Why is no real title available?)
• scientific article; zbMATH DE number 3318613 (Why is no real title available?)
• A Definition of Ordinal Numbers
• A theorem on n-tuples which is equivalent to the well-ordering theorem
• Automated deduction in von Neumann-Bernays-Gödel set theory
• Axiomatic set theory. With a historical introduction by Abraham A. Fraenkel
• Computer proofs in Gödel's class theory with equational definitions for composite and cross
• Consistency of the Continuum Hypothesis. (AM-3)
• Experimenting with Isabelle in ZF set theory
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• On computer-assisted proofs in ordinal number theory
• On equivalents of well-foundedness. An experiment in MIZAR
• Set theory in first-order logic: Clauses for Gödel's axioms

Cited in

(2)

• Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
• A formalisation of finite automata using hereditarily finite sets

Describes a project that uses

Uses Software

• Metamath
• OTTER

This page was built for publication: Computer proofs about finite and regular sets: The unifying concept of subvariance.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1404990)