CADE 1997 | Sciweavers

23

CADE
1997
Springer

134views Logical Reasoning» more CADE 1997»

A Classification of Non-liftable Orders for Resolution

13 years 11 months ago

In this paper we study the completeness of resolution when it is restricted by a non-liftable order and by weak subsumption. A non-liftable order is an order that does not satisfy...

Hans de Nivelle

claim paper

Read More »

28

click to vote

CADE
1997
Springer

153views Logical Reasoning» more CADE 1997»

Automatic Verification of Cryptographic Protocols with SETHEO

13 years 11 months ago

Download ti.arc.nasa.gov

Johann Schumann

claim paper

Read More »

28

click to vote

CADE
1997
Springer

160views Logical Reasoning» more CADE 1997»

Connection-Based Proof Construction in Linear Logic

13 years 11 months ago

Download www.cs.cornell.edu

We present a matrix characterization of logical validity in the multiplicative fragment of linear logic. On this basis we develop a matrix-based proof search procedure for this fra...

Christoph Kreitz, Heiko Mantel, Jens Otten, Stepha...

claim paper

Read More »

25

click to vote

CADE
1997
Springer

191views Logical Reasoning» more CADE 1997»

Deciding Intuitionistic Propositional Logic via Translation into Classical Logic

13 years 11 months ago

Download www.cs.cornell.edu

Abstract. We present a technique that eﬃciently translates propositional intuitionistic formulas into propositional classical formulas. This technique allows the use of arbitrary...

Daniel S. Korn, Christoph Kreitz

claim paper

Read More »

48

click to vote

CADE
1997
Springer

313views Logical Reasoning» more CADE 1997»

Nuprl-Light: An Implementation Framework for Higher-Order Logics

13 years 11 months ago

Download files.metaprl.org

Jason J. Hickey

claim paper