Building Theorem Provers

被引：0

作者：

Stickel, Mark E. ^{[1
]}

机构：

[1] SRI Int, Ctr Artificial Intelligence, Menlo Pk, CA 94025 USA

来源：

AUTOMATED DEDUCTION - CADE-22 | 2009年 / 5663卷

关键词：

UNIFICATION ALGORITHM; RESOLUTION; SETS;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

This talk discusses some of the challenges of building a usable theorem prover. These include the chasm between theory and code, conflicting requirements, feature interaction, and competitive performance. The talk draws on the speaker's experiences with devising extensions of resolution and building theorem provers that have been used as embedded reasoners in various systems.

引用

页码：306 / 321

页数：16

共 45 条

[1] Logic-based subsumption architecture [J].

Amir, E ;

Maynard-Zhang, P .

ARTIFICIAL INTELLIGENCE, 2004, 153 (1-2) :167-237

[2]

[Anonymous], 2003, DESCRIPTION LOGIC HD

[3]

[Anonymous], 2004, Knowledge representation and reasoning

[4]

[Anonymous], MANY SORTED CALCULUS

[5]

[Anonymous], 1963, Computers and Thought

[6]

[Anonymous], 1978, Automated Theorem Proving: A Logical Basis

[7]

Baader F., 1998, Term rewriting and all that

[8]

Chang C.-L., 1973, Symbolic Logic and Mechanical Theorem Proving, DOI DOI 10.1137/1016071

[9]

Dantsin E, 1999, LECT NOTES COMPUT SC, V1578, P180

[10] Z-RESOLUTION - THEOREM-PROVING WITH COMPILED AXIOMS [J].

DIXON, JK .

JOURNAL OF THE ACM, 1973, 20 (01) :127-147

← 1 2 3 4 5 →