Project Page Index Table of Contents
  • Satisfiability of elementary, square, and uniform Diophantine constraints H10C_SAT, H10SQC_SAT, and H10UC_SAT
    • HaltMTM and HaltTM 1 are undecidable
    • SBTM_HALT is enumerable
    • complement SBTM_HALT is undecidable
    • SBTM_HALT is undecidable
  • Validity, provability, satisfiability of dyadic first-order logic
    • Dyadic validity, large fragment
    • Dyadic validity, small fragment without negation
    • Dyadic Kripke validity, small fragment without negation
    • Dyadic int. provability, small fragment without negation
    • Dyadic classical provability, small fragment without negation
    • Dyadic satisfiability, small fragment with negation
    • Dyadic Kripke satisfiability, small fragment with negation
    • Dyadic finite satisfiability, small fragment with negation
    • Dyadic finite validity, small fragment with negation
Generated by coqdoc and improved with CoqdocJS