Towards Completeness via Proof Search in the Linear Time μ-calculus

被引：3
|
作者：
Doumane, Amina [1 ,2 ]
Baelde, David [3 ,4 ]
Hirschi, Lucca [3 ,4 ]
Saurin, Alexis [1 ,2 ]
机构：
[1] CNRS, IRIF, PPS, Paris, France
[2] Univ Paris Diderot, Paris, France
[3] ENS Cachan, LSV, Cachan, France
[4] Univ Paris Saclay, CNRS, Paris, France
来源：
PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016) | 2016年
关键词：
mu-calculus; proof-search; sequent calculus; circular proofs; (co)induction; parity automata; safra construction;
D O I：
10.1145/2933575.2933598
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Modal mu-calculus is one of the central languages of logic and verification, whose study involves notoriously complex objects: automata over infinite structures on the model-theoretical side; infinite proofs and proofs by (co)induction on the proof-theoretical side. Nevertheless, axiomatizations have been given for both linear and branching time mu-calculi, with quite involved completeness arguments. We come back to this central problem, considering it from a proof search viewpoint, and provide some new completeness arguments in the linear time mu-calculus. Our results only deal with restricted classes of formulas that closely correspond to (non-alternating) omega-automata but, compared to earlier proofs, our completeness arguments are direct and constructive. We first consider a natural circular proof system based on sequent calculus, and show that it is complete for inclusions of parity automata expressed as formulas, making use of Safra's construction directly in proof search. We then consider the corresponding finitary proof system, featuring (co) induction rules, and provide a partial translation result from circular to finitary proofs. This yields completeness of the finitary proof system for inclusions of sufficiently deterministic parity automata, and finally for arbitrary Buchi automata.
引用
收藏
页码：377 / 386
页数：10
相关论文
共 50 条
  • [41] Unifying proof methodologies of duration calculus and timed linear temporal logic
    Liu, ZM
    Ravn, AR
    Li, XS
    FORMAL ASPECTS OF COMPUTING, 2004, 16 (02) : 140 - 154
  • [42] Towards a Calculus for Non-Linear Spectral Gaps
    Mendel, Manor
    Naor, Assaf
    PROCEEDINGS OF THE TWENTY-FIRST ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, 2010, 135 : 236 - +
  • [43] A FOCUSED SEQUENT CALCULUS FRAMEWORK FOR PROOF-SEARCH IN PURE TYPE SYSTEMS
    Lengrand, Stephane
    Dyckhoff, Roy
    McKinna, James
    LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (01)
  • [44] UPPER-BOUNDS FOR PROOF-SEARCH IN A SEQUENT CALCULUS FOR RELATIONAL EQUATIONS
    SCHONFELD, W
    ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1982, 28 (03): : 239 - 246
  • [45] Improving Refutational Completeness of Relational Search via Divergence Test
    Rozplokhas, Dmitri
    Boulytchev, Dmitri
    PPDP'18: PROCEEDINGS OF THE 20TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2018,
  • [46] On structuring proof search for first order linear logic
    Bruscoli, Paola
    Guglielmi, Alessio
    THEORETICAL COMPUTER SCIENCE, 2006, 360 (1-3) : 42 - 76
  • [47] Linear logic with Isabelle: Pruning the proof search tree
    deGroote, P
    THEOREM PROVING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1995, 918 : 263 - 277
  • [48] On structuring proof search for first order linear logic
    Bruscoli, P
    Guglielmi, A
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2003, 2850 : 389 - 406
  • [49] Efficient resource management for linear logic proof search
    Cervesato, I
    Hodas, JS
    Pfenning, F
    THEORETICAL COMPUTER SCIENCE, 2000, 232 (1-2) : 133 - 163
  • [50] Propositional intuitionistic multiple-conclusion calculus via proof graphs
    Carvalho, Ruan V. B.
    de Oliveira, Anjolina G.
    de Queiroz, Ruy J. G. B.
    LOGIC JOURNAL OF THE IGPL, 2019, 27 (01) : 33 - 59
12345