Integrating constraint solving into proof planning

被引:0
|
作者
Melis, E [1 ]
Zimmer, J
Müller, T
机构
[1] Univ Saarland, Fachbereich Informat, D-66041 Saarbrucken, Germany
[2] Univ Saarland, Programming Syst Lab, D-66041 Saarbrucken, Germany
来源
关键词
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers into proof planning can sometimes help solving this problem. We present such an integration and discover certain requirements to be met in order to integrate the constraint solver's efficient activities in a way that is correct and sufficient for proof planning. We explain how the requirements can be met by n extension of the constraint solving technology and describe their implementation in the constraint solver CoSIE.
引用
下载
收藏
页码:32 / 46
页数:15
相关论文
共 50 条
  • [41] A New Method of Solving UAV Trajectory Planning Under Obstacles and Multi-Constraint
    Shao, Shikai
    Shi, Weilong
    Zhao, Yuanjie
    Du, Yun
    IEEE ACCESS, 2021, 9 : 161161 - 161180
  • [42] Constraint propagation as a proof system
    Atserias, A
    Kolaitis, PG
    Vardi, MY
    PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING - CP 2004, PROCEEDINGS, 2004, 3258 : 77 - 91
  • [43] Proof Logging for the Circuit Constraint
    McIlree, Matthew J.
    McCreesh, Ciaran
    Nordstrom, Jakob
    INTEGRATION OF CONSTRAINT PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND OPERATIONS RESEARCH, PT II, CPAIOR 2024, 2024, 14743 : 38 - 55
  • [44] Integrating Abduction and Constraint Optimization in Constraint Handling Rules
    Gavanelli, Marco
    Alberti, Marco
    Lamma, Evelina
    ECAI 2008, PROCEEDINGS, 2008, 178 : 903 - +
  • [45] Integrating ACO and constraint propagation
    Meyer, B
    Ernst, A
    ANT COLONY OPTIMIZATION AND SWARM INTELLIGENCE, PROCEEDINGS, 2004, 3172 : 166 - 177
  • [46] Soft constraint propagation and solving in constraint handling rules
    Bistarelli, S
    Frühwirth, T
    Marte, M
    Rossi, F
    COMPUTATIONAL INTELLIGENCE, 2004, 20 (02) : 287 - 307
  • [47] Program Analysis as Constraint Solving
    Gulwani, Sumit
    Srivastava, Saurabh
    Venkatesan, Ramarathnam
    PLDI'08: PROCEEDINGS OF THE 2008 SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN & IMPLEMENTATION, 2008, : 281 - +
  • [48] Symbolic Automata Constraint Solving
    Veanes, Margus
    Bjorner, Nikolaj
    de Moura, Leonardo
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, 2010, 6397 : 640 - 654
  • [49] Predictive Constraint Solving and Analysis
    Almaawi, Alyas
    Dini, Nima
    Yelen, Cagdas
    Gligoric, Milos
    Misailovic, Sasa
    Khurshid, Sarfraz
    2020 IEEE/ACM 42ND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: NEW IDEAS AND EMERGING RESULTS (ICSE-NIER 2020), 2020, : 109 - 112
  • [50] Solving Sudoku with Constraint Programming
    Crawford, Broderick
    Castro, Carlos
    Monfroy, Eric
    CUTTING-EDGE RESEARCH TOPICS ON MULTIPLE CRITERIA DECISION MAKING, PROCEEDINGS, 2009, 35 : 345 - +