A Complete Proof System for First-order Interval Temporal Logic with Projection

2004 ◽  
Vol 14 (2) ◽  
pp. 215-249 ◽  
Author(s):  
D. P. Guelev
Keyword(s):  
Temporal Logic ◽  
Proof System ◽  
Order Interval ◽  
Complete Proof ◽  
First Order ◽  
Interval Temporal Logic

A sound and complete proof system for a unified temporal logic

2020 ◽  
Vol 838 ◽  
pp. 25-44
Author(s):  
Liang Zhao ◽  
Xiaobing Wang ◽  
Xinfeng Shu ◽  
Nan Zhang
Keyword(s):  
Temporal Logic ◽  
Proof System ◽  
Complete Proof

scholarly journals A complete proof system for propositional projection temporal logic

2013 ◽  
Vol 497 ◽  
pp. 84-107 ◽  
Author(s):  
Zhenhua Duan ◽  
Nan Zhang ◽  
Maciej Koutny
Keyword(s):  
Temporal Logic ◽  
Proof System ◽  
Complete Proof

Towards the Temporal Approach to Abstract Data Types

1988 ◽  
Vol 11 (1) ◽  
pp. 49-63
Author(s):  
Andrzej Szalas
Keyword(s):  
Temporal Logic ◽  
Abstract Data Types ◽  
Data Types ◽  
First Order ◽  
Abstract Data ◽  
Order Completeness ◽  
General Method

In this paper we deal with a well known problem of specifying abstract data types. Up to now there were many approaches to this problem. We follow the axiomatic style of specifying abstract data types (cf. e.g. [1, 2, 6, 8, 9, 10]). We apply, however, the first-order temporal logic. We introduce a notion of first-order completeness of axiomatic specifications and show a general method for obtaining first-order complete axiomatizations. Some examples illustrate the method.

A Complete Proof System for SCCS with Modal Assertions

1986 ◽  
Vol 9 (4) ◽  
pp. 401-419
Author(s):  
Glynn Winskel
Keyword(s):  
Proof System ◽  
Complete Proof

scholarly journals Constructing weak simulations from linear implications for processes with private names

2019 ◽  
Vol 29 (8) ◽  
pp. 1275-1308 ◽  
Author(s):  
Ross Horne ◽  
Alwen Tiu
Keyword(s):  
Expressive Power ◽  
Dual Pair ◽  
Proof System ◽  
Branching Time ◽  
First Order ◽  
Order Extension

AbstractThis paper clarifies that linear implication defines a branching-time preorder, preserved in all contexts, when used to compare embeddings of process in non-commutative logic. The logic considered is a first-order extension of the proof system BV featuring a de Morgan dual pair of nominal quantifiers, called BV1. An embedding of π-calculus processes as formulae in BV1 is defined, and the soundness of linear implication in BV1 with respect to a notion of weak simulation in the π -calculus is established. A novel contribution of this work is that we generalise the notion of a ‘left proof’ to a class of formulae sufficiently large to compare embeddings of processes, from which simulating execution steps are extracted. We illustrate the expressive power of BV1 by demonstrating that results extend to the internal π -calculus, where privacy of inputs is guaranteed. We also remark that linear implication is strictly finer than any interleaving preorder.

Sign in / Sign up

Export Citation Format

Share Document