Proceedings - Symposium on Logic in Computer Science

Công bố khoa học tiêu biểu

* Dữ liệu chỉ mang tính chất tham khảo

Sắp xếp:  
Modal and guarded characterisation theorems over finite transition systems
Proceedings - Symposium on Logic in Computer Science - - Trang 371-380
M. Otto
Characterisation theorems for modal and guarded fragments of first-order logic are explored over finite transition systems. We show that the classical characterisations in terms of semantic invariance under the appropriate forms of bisimulation equivalence can be recovered at the level of finite model theory. The new, more constructive proofs naturally extend to alternative proofs of the classical...... hiện toàn bộ
#Logic #H infinity control #Game theory #Computer science
The powerdomain of indexed valuations
Proceedings - Symposium on Logic in Computer Science - - Trang 299-308
D. Varacca
This paper is about combining nondeterminism and probabilities. We study this phenomenon from a domain theoretic point of view. In domain theory, nondeterminism is modeled using the notion of powerdomain, while probability is modeled using the powerdomain of valuations. Those two functors do not combine well, as they are. We define the notion of powerdomain of indexed valuations, which can be comb...... hiện toàn bộ
#Cost accounting #Equations #Computer science #Laboratories #Computational modeling #Probability distribution #Algebra #Logic #Character generation
The 0-1 law fails for frame satisfiability of propositional modal logic
Proceedings - Symposium on Logic in Computer Science - - Trang 225-234
J.-M. Le Bars
The digraph property KERNEL is a very simple and wellknown property studied in various areas. We previously defined a variant of this property as a counterexample of 0-1 law for the monadic existential second order logic with at most two first-order variables, over structures with 16 binary relations. Goranko and Kapron have defined two variants in frames which expresses frame satisfiability of pr...... hiện toàn bộ
#Logic #Kernel #Vocabulary #Bars #Computational modeling #Computational complexity #Combinatorial mathematics #H infinity control
Semantics and logic of object calculi
Proceedings - Symposium on Logic in Computer Science - - Trang 113-122
B. Reus, T. Streicher
The main contribution of this paper is a formal characterization of recursive object specifications based on a denotational untyped semantics of the object calculus and the discussion of existence of those (recursive) specifications. The semantics is then applied to prove soundness of a programming logic for the object calculus and to suggest possible extensions. For the purposes of this discussio...... hiện toàn bộ
#Logic programming #Calculus #Object oriented programming #Machinery #Object oriented modeling #Computer science
Games on graphs and sequentially realizable functionals. Extended abstract
Proceedings - Symposium on Logic in Computer Science - - Trang 257-264
M. Hyland, A. Schalk
We present a new category of games on graphs and derive from it a model for Intuitionistic Linear Logic. Our category has the computational flavour of concrete data structures but embeds fully and faithfully in an abstract games model. It differs markedly from the usual Intuitionistic Linear Logic setting for sequential algorithms. However, we show that with a natural exponential we obtain a model...... hiện toàn bộ
#Logic #Concrete #Computer science #Data structures #Mathematical model #Embedded computing #Algorithm design and analysis #Tree graphs
On the lambda Y calculus
Proceedings - Symposium on Logic in Computer Science - - Trang 159-166
R. Statman
In this paper we consider three problems concerning the lambda Y calculus obtained from the simply typed lambda calculus by the addition of fixed point combinators Y: (A/spl rarr/A)/spl rarr/A. The "paradoxical" combinator Y was first discussed in by Curry & Feys Vol 1 (1958). It appears first in a typed context by A. Scott (1969) and also by R. Platek's thesis (1963), and forms the basis for L. C...... hiện toàn bộ
#Calculus #Magnetic heads #Encoding #Equations #Logic #Computer science #Standardization
The proof complexity of linear algebra
Proceedings - Symposium on Logic in Computer Science - - Trang 335-344
M. Soltys, S. Cook
We introduce three formal theories of increasing strength for linear algebra in order to study the complexity of the concepts needed to prove the basic theorems of the subject. We give what is apparently the first feasible proofs of the Cayley-Hamilton theorem and other properties of the determinant, and study the propositional proof complexity of matrix identities.
#Linear algebra #Matrices #Polynomials #Computer science #Educational institutions #Parallel algorithms #Galois fields #Lagrangian functions #Logic
Decidable and undecidable fragments of first-order branching temporal logics
Proceedings - Symposium on Logic in Computer Science - - Trang 393-402
I. Hodkinson, F. Wolter, M. Zakharyaschev
In this paper we analyze the decision problem for fragments of first-order extensions of branching time temporal logics such as computational tree logics CTL and CTL* or Prior's Ockhamist logic of historical necessity. On the one hand, we show that the one-variable fragments of logics like first-order CTL*-such as the product of propositional CTL* with simple propositional modal logic S5, or even ...... hiện toàn bộ
#Logic #Computer science #Educational institutions #Knowledge representation #Application software #Turning #History
The metric analogue of weak bisimulation for probabilistic processes
Proceedings - Symposium on Logic in Computer Science - - Trang 413-422
J. Desharnais, R. Jagadeesan, V. Gupta, P. Panangaden
We observe that equivalence is not a robust concept in the presence of numerical information - such as probabilities-in the model. We develop a metric analogue of weak bisimulation in the spirit of our earlier work on metric analogues for strong bisimulation. We give a fixed point characterization of the metric. This makes available conductive reasoning principles and allows us to prove metric ana...... hiện toàn bộ
#Computer science #Probability distribution #Robustness #Channel capacity #Concurrent computing #Distributed computing #Stochastic systems #State-space methods #Logic #Boolean functions
Unsatisfiable random formulas are hard to certify
Proceedings - Symposium on Logic in Computer Science - - Trang 325-334
A. Atserias
We prove that every property of 3CNF formulas that implies unsatisfiability and is expressible in Datalog has asymptotic probability zero when formulas are randomly generated by taking 6n non-trivial clauses of exactly three literals uniformly and independently. Our result is a consequence of designing a winning strategy for Duplicator in the existential k-pebble game on the structure that encodes...... hiện toàn bộ
#Encoding #Computational complexity #Polynomials #Calculus #Logic #Computer science
Tổng số: 42   
  • 1
  • 2
  • 3
  • 4
  • 5