Deciding simple infinity axiom sets with one binary relation by means of superpostulates

DOI10.1007/978-3-030-51074-9_12MaRDI QIDQ2096446zbMATH OpenOpenAlexFDO

Authors Timm Lampert, Anderson Nakano

Publication date 9 November 2022

Full work available at URL https://doi.org/10.1007/978-3-030-51074-9_12

zbMATH Keywords

complete theoriesdecision problemdyadic logicfirst-order logicinfinity axiomsreduction classes

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• An infinity of super-Belnap logics
• Decidability of the existential theory of infinite terms with subterm relation
• Hyperhypersimple supersets in admissible recursion theory
• Note on "The Logically Simplest Form of the Infinity Axiom"
• Decidability of the binary infinite Post Correspondence Problem
• The Logically Simplest Form of the Infinity Axiom
• THE DECISION PROBLEM FOR RESTRICTED UNIVERSAL QUANTIFICATION IN SET THEORY AND THE AXIOM OF FOUNDATION
• Relative consistency of the general axiom of superuniversality for sets, \(n\)-tuples and operations
• Undecidability of the problem of recognizing axiomatizations of superintuitionistic propositional calculi
• Expressive power of infinitary \([0,1]\)-logics

Cites work

• Automated inference of finite unsatisfiability
• Computability and Logic
• Finite axiomatizability and theories with trivial algebraic closure
• Henry M. Sheffer and notational relativity
• scientific article; zbMATH DE number 3715502 (Why is no real title available?)
• scientific article; zbMATH DE number 3248792 (Why is no real title available?)
• scientific article; zbMATH DE number 3334141 (Why is no real title available?)
• Minimizing disjunctive normal forms of pure first-order logic
• On first-order sentences without finite models
• The classical decision problem.

Cited in

(1)

• The 10th IJCAR automated theorem proving system competition -- CASC-J10

This page was built for publication: Deciding simple infinity axiom sets with one binary relation by means of superpostulates

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