{
  "annotation_id": "62137d6e-0f89-434d-9a1d-ddda81506e46",
  "date_created": "2026-02-17T05:53:24.090000Z",
  "date_modified": "2026-02-17T05:53:24.090000Z",
  "file_hash": "01446572299b2b9f267ba0a6e5c3964d892dfc4d9decd67f5d6f6585efbdc1bc",
  "private": false,
  "record": {
    "abstract": "In this paper, we introduce a Ketonen-type Gentzen-style classical simple type theory $\\bf KCT$. Also the tableau system $\\bf KCTT$ corresponding to $\\bf KCT$ is introduced. Further inference-preserving Gentzen system $\\bf KCT_h$ (equivalent to $\\bf KCT$) and tableau system $\\bf KCTT_h$ (equivalent to $\\bf KCTT$) is introduced. We introduce the notion of Hintikka sequents for $\\bf KCTT_h$.The completeness theorem and Takahashi-Prawitz\u0027s theorem are proved for $\\bf KCTT_h$.",
    "arxiv_id": "2601.10026",
    "authors": [
      "Tadayoshi Miwa",
      "Takao Inou\u00e9"
    ],
    "categories": [
      "math.LO"
    ],
    "license": "http://arxiv.org/licenses/nonexclusive-distrib/1.0/",
    "title": "A New Overture to Classical Simple Type Theory, Ketonen-type Gentzen and Tableau Systems",
    "url": "https://arxiv.org/abs/2601.10026",
    "version": "v1"
  },
  "schema_id": "dorsal/arxiv",
  "source": {
    "execution_id": "4c6c8a59-9d77-4c3e-8438-350448262fa5",
    "id": "arXiv Dataset",
    "type": "Model",
    "variant": "snapshot-2026-01-17",
    "version": "0.1.0"
  },
  "user_id": 1000002
}