A Decision Method for First-Order Stream Logic

被引：0

作者：

Ruess, Harald ^{[1
]}

机构：

[1] Entalus Comp Sci Lab, 2071 Gulf Mexico Dr, Longboat Key, FL 34228 USA

来源：

AUTOMATED REASONING, IJCAR 2024, PT II | 2024年 / 14740卷

关键词：

Decision Procedures; First-Order Logic; Stream Calculus; Formal Power Series; Real-Closed Rings; Quantifier Elimination; QUANTIFIER ELIMINATION; REAL; DEFINABILITY; SERIES; RINGS;

D O I：

10.1007/978-3-031-63501-4_8

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Our main result is a doubly exponential decision procedure for the first-order equality theory of streams with addition, convolution, and control-oriented stream operations. This stream logic is shown to be expressive for solving basic problems in stream calculus.

引用

页码：137 / 156

页数：20

共 47 条

[1]

Alling N., 1987, Foundations of Analysis over Surreal Number Fields

[2]

Allouche J-P., 2003, AUTOMATIC SEQUENCES, DOI [10.1017/CBO9780511546563, DOI 10.1017/CBO9780511546563]

[3] AN EXISTENTIAL O-DEFINITION OF Fq[[t]] IN Fq((t)) [J].

Anscombe, Will ;

Koenigsmann, Jochen .

JOURNAL OF SYMBOLIC LOGIC, 2014, 79 (04) :1336-1343

[4] ON UNDECIDABILITY OF POWER SERIES FIELDS [J].

AX, J .

PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY, 1965, 16 (04) :846-&

[5] On the combinatorial and algebraic complexity of quantifier elimination [J].

Basu, S ;

Pollack, R ;

Roy, MF .

JOURNAL OF THE ACM, 1996, 43 (06) :1002-1045

[6]

Bourbaki N., 1964, Elements de mathematique: Fasc. I. Livre 1, Theorie des ensembles

[7]

[5], Fascicule de resultats

[8]

Broy M., 2001, Specification and development of interactive systems: Focus on streams, interfaces, and refinement, DOI DOI 10.1007/978-1-4613-0091-5

[9] Specification and verification of concurrent systems by causality and realizability [J].

Broy, Manfred .

THEORETICAL COMPUTER SCIENCE, 2023, 974

[10] DEFINABILITY IN MONADIC SECOND-ORDER THEORY OF SUCCESSOR [J].

BUCHI, JR ;

LANDWEBE.LH .

JOURNAL OF SYMBOLIC LOGIC, 1969, 34 (02) :166-&

← 1 2 3 4 5 →