A tableau calculus for first-order branching time logic | Zendy

Wolfgang May | Zendy; Peter H. Schmitt | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A tableau calculus for first-order branching time logic

Author(s) -

Wolfgang May,

Peter H. Schmitt

Publication year - 1996

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-61313-7

DOI - 10.1007/3-540-61313-7_89

Subject(s) - calculus (dental) , computer science , computation tree logic , temporal logic , process calculus , ctl* , representation (politics) , model checking , propositional calculus , first order logic , mathematics , discrete mathematics , algorithm , theoretical computer science , biochemistry , chemistry , cytotoxic t cell , politics , political science , law , in vitro , medicine , dentistry

. Tableau-based proof systems have been designed for manylogics extending classical first-order logic. This paper proposes a soundtableau calculus for temporal logics of the first-order CTL-family. Untilnow, a tableau calculus has only been presented for the propositionalversion of CTL. The calculus considered operates with prefixed formulasand may be regarded as an instance of a labelled deductive system. Theprefixes allow an explicit partial description of states and paths of a...

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research