Set theory in first-order logic: Clauses for Gödel's axioms

DOI10.1007/BF02328452zbMATH Open0635.03008OpenAlexW1966945932WikidataQ114264489 ScholiaQ114264489MaRDI QIDQ1097252FDOQ1097252

Authors: B. George 

Publication date: 1986

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

Full work available at URL: https://doi.org/10.1007/bf02328452

Recommendations

• Automated deduction in von Neumann-Bernays-Gödel set theory
• Computational logic and set theory. Applying formalized logic to analysis. Foreword by Martin Davis
• scientific article; zbMATH DE number 158462
• An automated prover for Zermelo-Fraenkel set theory in Theorema
• scientific article; zbMATH DE number 1614691

zbMATH Keywords

number theoryresolution-based automated theorem provingset of clauses for set theoryGödel's formulation of set theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Set theory (03E99)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Splitting and reduction heuristics in automatic theorem proving
• Title not available (Why is that?)

Cited In (25)

• Title not available (Why is that?)
• The application of automated reasoning to formal models of combinatorial optimization
• The problem of demodulating across argument and literal boundaries
• A Mizar mode for HOL
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Layered map reasoning: an experimental approach put to trial on sets
• Computer proofs about finite and regular sets: The unifying concept of subvariance.
• The TPTP problem library
• Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Reasoning about iteration in Gödel's class theory.
• Experimenting with Isabelle in ZF set theory
• The kernel strategy and its use for the study of combinatory logic
• Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
• Set theory for verification. I: From foundations to functions
• A derived algorithm for evaluating \(\varepsilon\)-expressions over abstract sets
• ILF-SETHEO
• TPS: A theorem-proving system for classical type theory
• Term rewriting: Some experimental results
• Automated deduction in von Neumann-Bernays-Gödel set theory
• Issues in commonsense set theory
• A finitely axiomatized formalization of predicate calculus with equality
• On sets, types, fixed points, and checkerboards
• Title not available (Why is that?)

This page was built for publication: Set theory in first-order logic: Clauses for Gödel's axioms

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