Computational Logic and Set Theory

DOI10.1007/978-0-85729-808-9zbMath1246.03006OpenAlexW2497601262MaRDI QIDQ5198513

Jacob T. Schwartz, Domenico Cantone, Eugenio Giovanni Omodeo

Publication date: 8 August 2011

Full work available at URL: https://doi.org/10.1007/978-0-85729-808-9

zbMATH Keywords

undecidabilityautomated reasoningdecidabilityset theorycomputational logicautomated theorem provingcomplex analysisCauchy integral theoremdecision proceduresincompleteness theoremsproof verifiersverifier \texttt{ÆtnaNova}

Mathematics Subject Classification ID

Integration, integrals of Cauchy type, integral representations of analytic functions in the complex plane (30E20) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Set theory (03E99)

Related Items

Set graphs. IV. Further connections with claw-freeness ⋮ Set-syllogistics meet combinatorics ⋮ Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages ⋮ A decidable theory involving addition of differentiable real functions ⋮ Unnamed Item ⋮ Complexity assessments for decidable fragments of set theory. II: A taxonomy for `small' languages involving membership ⋮ A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions ⋮ Banishing Ultrafilters from Our Consciousness ⋮ Martin Davis’s Bibliography 1950–2015 ⋮ Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case* ⋮ Applicable Mathematics in a Minimal Computational Theory of Sets ⋮ Formative processes with applications to the decision problem in set theory. II. Powerset and singleton operators, finiteness predicate ⋮ Set graphs. II. Complexity of set graph recognition and similar problems ⋮ The decision problem for a three-sorted fragment of set theory with restricted quantification and finite enumerations ⋮ A Set-theoretic Approach to Reasoning Services for the Description Logic 𝒟 ℒ D 4,× ⋮ An Improved Set-based Reasoner for the Description Logic 𝒟ℒD4,׆ ⋮ NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF ⋮ Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets

Uses Software

• AEtnaNova

This page was built for publication: Computational Logic and Set Theory