CADE 2001 - PDF Preprint Papers

CADE 2001 Automated Deduction

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed CADE-2001 Paper

click to vote

CADE
2001
Springer

185views Logical Reasoning» more CADE 2001»

A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities

14 years 4 months ago

Download i12www.ira.uka.de

The modalities of Dynamic Logic refer to the final state of a program execution and allow to specify programs with pre- and postconditions. In this paper, we extend Dynamic Logic w...

Bernhard Beckert, Steffen Schlager

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	185	A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities	claim
2	181	NEXPTIME-Complete Description Logics with Concrete Domains	claim
3	179	Context Trees	claim
4	176	Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems	claim
5	161	NoMoRe : A System for Non-monotonic Reasoning with Logic Programs under Answer Set Semantics	claim
6	157	Termination and Reduction Checking for Higher-Order Logic Programs	claim
7	146	Canonical Propositional Gentzen-Type Systems	claim
8	141	More On Implicit Syntax	claim
9	140	RACER System Description	claim
10	135	A Top-Down Procedure for Disjunctive Well-Founded Semantics	claim
11	133	Approximating Dependency Graphs Using Tree Automata Techniques	claim
12	128	JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants	claim
13	127	Incremental Closure of Free Variable Tableaux	claim
14	112	Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics	claim
15	111	Hilberticus - A Tool Deciding an Elementary Sublanguage of Set Theory	claim
16	110	STRIP: Structural Sharing for Efficient Proof-Search	claim
17	108	SET Cardholder Registration: The Secrecy Proofs	claim
18	107	NP-Completeness of Refutability by Literal-Once Resolution	claim
19	106	A New Meta-complexity Theorem for Bottom-Up Logic Programs	claim
20	105	A Model-Based Completeness Proof of Extended Narrowing and Resolution	claim
21	101	On the Evaluation of Indexing Techniques for Theorem Proving	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers