Paper Info
Title
Binary Extensions of S1S and the Composition Method
Abstract
The study of the decidability of the so-called sequential calculus S1S calls into play two techniques employing tools at the heart of Logic and Computer Science: Buchi automata on infinite words [1] and Shelah's composition method [10]. In this paper we continue along the line started by Thomas in [14] and we compare the decidability proofs for S1S also in a case in which the basic endowment of interpreted predicates is not restricted to <, but it is extended with a binary operator. In particular, we outline how the composition method can be successfully applied to give an alternative proof of the decidability of the proper extension of S1S with the binary predicate flip (see [9] and the following sections(1)).
Year
DOI
Venue
2003
10.1007/978-3-540-39910-0_27
LECTURE NOTES IN COMPUTER SCIENCE
Field
DocType
Volume
Atomic formula,Discrete mathematics,Closure (mathematics),Computer science,Decidability,Mathematical proof,Predicate (grammar),Binary operation,Binary number,Büchi automaton
Conference
2772
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
6
3
Name
Order
Citations
PageRank
Enrico Marzano1123.21
Angelo Montanari21535135.04
Alberto Policriti378574.35