Automated Deduction—CADE-18 - Lecture Notes in Computer Science
Latest Publications

TOTAL DOCUMENTS

(FIVE YEARS 0)

H-INDEX

(FIVE YEARS 0)

Published By Springer Berlin Heidelberg

9783540439318, 9783540456209

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Formal Verification of a Combination Decision Procedure

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_29 ◽

2002 ◽

pp. 347-362 ◽

Cited By ~ 9

Author(s):

Jonathan Ford ◽

Natarajan Shankar

Keyword(s):

Formal Verification ◽

Decision Procedure

Download Full-text

Deductive Search for Errors in Free Data Type Specifications Using Model Generation

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_18 ◽

2002 ◽

pp. 211-225 ◽

Cited By ~ 7

Author(s):

Wolfgang Ahrendt

Keyword(s):

Data Type ◽

Model Generation ◽

Free Data

Download Full-text

Temporal Logic for Proof-Carrying Code

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_3 ◽

2002 ◽

pp. 31-46 ◽

Cited By ~ 8

Author(s):

Andrew Bernard ◽

Peter Lee

Keyword(s):

Temporal Logic

Download Full-text

Proof Development with Ωmega

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_12 ◽

2002 ◽

pp. 144-149 ◽

Cited By ~ 20

Author(s):

Jörg Siekmann ◽

Christoph Benzmüller ◽

Vladimir Brezhnev ◽

Lassaad Cheikhrouhou ◽

Armin Fiedler ◽

...

Download Full-text

An LCF-Style Interface between HOL and First-Order Logic

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_10 ◽

2002 ◽

pp. 134-138 ◽

Cited By ~ 15

Author(s):

Joe Hurd

Keyword(s):

Order Logic ◽

First Order Logic ◽

First Order

Download Full-text

Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_36 ◽

2002 ◽

pp. 456-470 ◽

Cited By ~ 3

Author(s):

Miquel Bofill ◽

Albert Rubio

Keyword(s):

Well Foundedness

Download Full-text

Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_35 ◽

2002 ◽

pp. 438-455 ◽

Cited By ~ 50

Author(s):

Leonardo de Moura ◽

Harald Rueß ◽

Maria Sorea

Keyword(s):

Model Checking ◽

Theorem Proving ◽

Bounded Model Checking ◽

Infinite Domains

Download Full-text

A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_4 ◽

2002 ◽

pp. 47-62 ◽

Cited By ~ 4

Author(s):

Robert R. Schneck ◽

George C. Necula

Keyword(s):

Gradual Approach

Download Full-text

Solving for Set Variables in Higher-Order Theorem Proving

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_33 ◽

2002 ◽

pp. 408-422 ◽

Cited By ~ 4

Author(s):

Chad E. Brown

Keyword(s):

Theorem Proving ◽

Higher Order

Download Full-text

Shostak Light

Automated Deduction—CADE-18 - Lecture Notes in Computer Science ◽

10.1007/3-540-45620-1_28 ◽

2002 ◽

pp. 332-346 ◽

Cited By ~ 16

Author(s):

Harald Ganzinger

Download Full-text

Automated Deduction—CADE-18 - Lecture Notes in Computer ScienceLatest Publications

TOTAL DOCUMENTS

H-INDEX

Published By Springer Berlin Heidelberg

Formal Verification of a Combination Decision Procedure

Deductive Search for Errors in Free Data Type Specifications Using Model Generation

Temporal Logic for Proof-Carrying Code

Proof Development with Ωmega

An LCF-Style Interface between HOL and First-Order Logic

Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation

Lazy Theorem Proving for Bounded Model Checking over Infinite Domains

A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code

Solving for Set Variables in Higher-Order Theorem Proving

Shostak Light

Automated Deduction—CADE-18 - Lecture Notes in Computer Science
Latest Publications