Combining Proofs of Higher-Order and First-Order Automated Theorem Provers
作者： Christoph Benzmüller , Volker Sorge , Manfred Kerber , Mateja Jamnik
DOI:
关键词:
摘要:
arxiv.org参考文章(18)
Volker Sorge, Christoph Benzm, -Ants { An open approach at combining Interactive and Automated Theorem Proving ,(2002)
Peter F. Patel-Schneider, DLP System Description. Description Logics. ,(1998)
Manfred Kerber, On the Representation of Mathematical Concepts and their Translation into First-Order Logic ,(1999)
Christoph Benzmüller, Extensional Higher-Order Paramodulation and RUE-Resolution conference on automated deduction. pp. 399- 413 ,(1999) , 10.1007/3-540-48660-7_39
Alexandre Riazanov, Andrei Voronkov, Vampire 1.1 (System Description) international joint conference on automated reasoning. pp. 376- 380 ,(2001)
Christoph Benzmüller, Volker Sorge, Mateja Jamnik, Manfred Kerber, Can a Higher-Order and a First-Order Theorem Prover Cooperate? international conference on logic programming. pp. 415- 431 ,(2005) , 10.1007/978-3-540-32275-7_27
Jia Meng, Lawrence C. Paulson, Experiments on Supporting Interactive Proof Using Resolution international joint conference on automated reasoning. pp. 372- 384 ,(2004) , 10.1007/978-3-540-25984-8_28
Peter B. Andrews, Chad E. Brown, Set comprehension in church's type theory Carnegie Mellon University. ,(2004)
Jorg Denzinger, Dirk Fuchs, Cooperation of heterogeneous provers international joint conference on artificial intelligence. pp. 10- 15 ,(1999)
Geoff Sutcliffe, Christian Suttner, The TPTP Problem Library Journal of Automated Reasoning. ,vol. 21, pp. 177- 203 ,(1998) , 10.1023/A:1005806324129