Zobrazeno 1 - 10
of 24
pro vyhledávání: '"F.4.1, F.3.1"'
Autor:
Platzer, André, Tan, Yong Kiam
Publikováno v:
J. ACM 67(1), Article 6, 2020, 66 pages
This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analy
Externí odkaz:
http://arxiv.org/abs/1905.13429
Autor:
Moszkowski, Ben
Publikováno v:
Logical Methods in Computer Science, Volume 8, Issue 3 (August 13, 2012) lmcs:759
Interval Temporal Logic (ITL) is an established temporal formalism for reasoning about time periods. For over 25 years, it has been applied in a number of ways and several ITL variants, axiom systems and tools have been investigated. We solve the lon
Externí odkaz:
http://arxiv.org/abs/1207.3816
Publikováno v:
Logical Methods in Computer Science, Volume 8, Issue 2 (April 27, 2012) lmcs:934
The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriv
Externí odkaz:
http://arxiv.org/abs/1204.2386
Publikováno v:
EPTCS 81, 2012, pp. 30-46
We present an extension of the second-order logic AF2 with iso-style inductive and coinductive definitions specifically designed to extract programs from proofs a la Krivine-Parigot by means of primitive (co)recursion principles. Our logic includes p
Externí odkaz:
http://arxiv.org/abs/1203.6158
Autor:
Lee, Gyesik, Werner, Benjamin
Publikováno v:
Logical Methods in Computer Science, Volume 7, Issue 4 (November 23, 2011) lmcs:920
We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's trace enco
Externí odkaz:
http://arxiv.org/abs/1111.0123
Publikováno v:
Logical Methods in Computer Science, Volume 7, Issue 3 (August 11, 2011) lmcs:784
The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we intr
Externí odkaz:
http://arxiv.org/abs/1105.2246
Publikováno v:
Logical Methods in Computer Science, Volume 8, Issue 2 (July 31, 2012) lmcs:1085
For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approxi
Externí odkaz:
http://arxiv.org/abs/1104.4983
Autor:
Demri, Stephane, Rabinovich, Alexander
Publikováno v:
Logical Methods in Computer Science, Volume 6, Issue 4 (December 21, 2010) lmcs:1230
We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamp's theorem. We show that it has a PSPACE-complete satisfiability problem over the cl
Externí odkaz:
http://arxiv.org/abs/1009.5206
Autor:
Halpern, Joseph Y., Moses, Yoram
This paper adds counterfactuals to the framework of knowledge-based programs of Fagin, Halpern, Moses, and Vardi. The use of counterfactuals is illustrated by designing a protocol in which an agent stops sending messages once it knows that it is safe
Externí odkaz:
http://arxiv.org/abs/cs/0311028
Autor:
Ben Moszkowski
Publikováno v:
Logical Methods in Computer Science, Vol Volume 8, Issue 3 (2012)
Interval Temporal Logic (ITL) is an established temporal formalism for reasoning about time periods. For over 25 years, it has been applied in a number of ways and several ITL variants, axiom systems and tools have been investigated. We solve the lon
Externí odkaz:
https://doaj.org/article/c41d1e9f2c364155831af53ea43e3a94
