CADE
1999
Springer
14 years 3 months ago
1999
Springer
We present a PSpace algorithm that decides satisfiability of the graded modal logic Gr(KR)—a natural extension of propositional modal logic KR by counting expressions—which pl...
CADE
1999
Springer
14 years 3 months ago
1999
Springer
Abstract. Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It rel...
CADE
1999
Springer
14 years 3 months ago
1999
Springer
CADE
1999
Springer
14 years 3 months ago
1999
Springer
We reduce the provability problem of any formula of the Lambek calculus to some context-free parsing problem. This reduction, which is based on non-commutative proof-net theory, al...
CADE
1999
Springer
14 years 3 months ago
1999
Springer
CADE
1999
Springer
14 years 3 months ago
1999
Springer
CADE
1999
Springer
14 years 3 months ago
1999
Springer
CutRes is a system which takes as input an LK-proof with arbitrary cuts and skolemized end-sequent and gives as output an LKproof with atomic cuts only. The elimination of cuts is ...