Automated theorem proving in first-order logic module: On the difference between type theory and set theory

被引：0
|
作者：
Dowek, G [1 ]
机构：
[1] Inst Natl Rech Informat & Automat, F-78153 Le Chesnay, France
来源：
AUTOMATED DEDUCTION IN CLASSICAL AND NON-CLASSICAL LOGICS | 2000年 / 1761卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Resolution modulo is a first-order theorem proving method that can be applied both to first-order presentations of simple type theory (also called higher-order logic) and to set theory. When it is applied to some first-order presentations of type theory, it simulates exactly higher-order resolution. In this note, we compare how it behaves on type theory and on set theory.
引用
收藏
页码：1 / 22
页数：22
相关论文
共 50 条
  • [21] First-order logic axiomatization of metric graph theory
    Chalopin, Jeremie
    Changat, Manoj
    Chepoi, Victor
    Jacob, Jeny
    THEORETICAL COMPUTER SCIENCE, 2024, 993
  • [22] AUTOMATIC THEOREM PROVING IN SET-THEORY
    PASTRE, D
    ARTIFICIAL INTELLIGENCE, 1978, 10 (01) : 1 - 27
  • [23] Automated theorem proving in quasigroup and loop theory
    Phillips, J. D.
    Stanovsky, David
    AI COMMUNICATIONS, 2010, 23 (2-3) : 267 - 283
  • [24] Comparing Unification Algorithms in First-Order Theorem Proving
    Hoder, Krystof
    Voronkov, Andrei
    KI 2009: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2009, 5803 : 435 - 443
  • [25] Predicate Elimination for Preprocessing in First-Order Theorem Proving
    Khasidashvili, Zurab
    Korovin, Konstantin
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2016, 2016, 9710 : 361 - 372
  • [26] APPROACH TO THEOREM PROVING IN TYPE THEORY
    ANDREWS, PB
    COHEN, EL
    JOURNAL OF SYMBOLIC LOGIC, 1979, 44 (03) : 477 - 478
  • [27] Holistic Deductive Framework Theorem Proving Based on Standard Contradiction Separation For First-Order Logic
    Cao, Feng
    Xu, Yang
    Zhong, Jian
    Wu, Guanfeng
    2017 12TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (IEEE ISKE), 2017,
  • [28] A 'theory' mechanism for a proof-verifier based on first-order set theory
    Omodeo, EG
    Schwartz, JT
    COMPUTATIONAL LOGIC: LOGIC PROGRAMMING AND BEYOND, PT II: ESSAYS IN HONOUR OF ROBERT A KOWALSKI, 2002, 2408 : 214 - 230
  • [29] Automated Generation of Consistent Graph Models with First-Order Logic Theorem Provers
    Babikian, Aren A.
    Semerath, Oszkar
    Varro, Daniel
    FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2020), 2020, 12076 : 441 - 461
  • [30] Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving
    Schneider, Michael
    Sutcliffe, Geoff
    AUTOMATED DEDUCTION - CADA-23, 2011, 6803 : 461 - 475
12345