Experimenting with Isabelle in ZF set theory

DOI10.1007/BF00881863zbMath0783.68109MaRDI QIDQ1312157

P. A. J. Noel

Publication date: 19 January 1994

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

zbMATH Keywords

set theoryIsabellebackward proofs

Mathematics Subject Classification ID

Axiomatics of classical set theory and its fragments (03E30)

Related Items

Set theory for verification. II: Induction and recursion ⋮ An approach to literate and structured formal developments ⋮ Computer proofs about finite and regular sets: The unifying concept of subvariance. ⋮ Layered map reasoning ⋮ Set theory for verification. I: From foundations to functions ⋮ The practice of logical frameworks

Uses Software

• Isabelle
• ETPS
• LCF
• Cambridge LCF

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Handbook of philosophical logic. Vol. I: Elements of classical logic
• Set theory in first-order logic: Clauses for Gödel's axioms
• The foundation of a generic theorem prover
• Logic and Computation