Towards the automation of set theory and its logic
From MaRDI portal
Publication:1253108
DOI10.1016/S0004-3702(78)80017-4zbMath0395.68082MaRDI QIDQ1253108
Publication date: 1978
Published in: Artificial Intelligence (Search for Journal in Brave)
Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04) Set theory (03Exx)
Related Items
Issues in commonsense set theory ⋮ MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics ⋮ Inductive reasoning on recursive equations ⋮ An investigation into the goals of research in automatic theorem proving as related to mathematical reasoning ⋮ A framework for using knowledge in tableau proofs ⋮ Une procédure de décision pour un problème de satisfiabilité dans un univers ensembliste héréditairement fini ⋮ Specification methods and partial construction of theory by computer ⋮ An experimental logic based on the fundamental deduction principle ⋮ Automatic theorem proving in set theory ⋮ Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions ⋮ Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\) ⋮ Set theory for verification. I: From foundations to functions ⋮ \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Mechanizing structural induction. II: Strategies
- Doing arithmetic without diagrams
- Automatic theorem proving in set theory
- Splitting and reduction heuristics in automatic theorem proving
- Computer proofs of limit theorems
- Toward Mechanical Mathematics
- An improved proof procedure1
- Proving Theorems about LISP Functions
- A Machine-Oriented Logic Based on the Resolution Principle
