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
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......
#Logic #H infinity control #Game theory #Computer science
The powerdomain of indexed valuations
Proceedings - Symposium on Logic in Computer Science - - Trang 299-308
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......
#Cost accounting #Equations #Computer science #Laboratories #Computational modeling #Probability distribution #Algebra #Logic #Character generation
Games on graphs and sequentially realizable functionals. Extended abstract
Proceedings - Symposium on Logic in Computer Science - - Trang 257-264
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......
#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
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......
#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
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
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 ......
#Logic #Computer science #Educational institutions #Knowledge representation #Application software #Turning #History
Unsatisfiable random formulas are hard to certify
Proceedings - Symposium on Logic in Computer Science - - Trang 325-334
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......
#Encoding #Computational complexity #Polynomials #Calculus #Logic #Computer science
A stratified semantics of general references embeddable in higher-order logic
Proceedings - Symposium on Logic in Computer Science - - Trang 75-86
We demonstrate a semantic model of general references - that is, mutable memory cells that may contain values of any (statically-checked) closed type, including other references. Our model is in terms of execution sequences on a von Neumann machine; thus, it can be used in a Proof-Carrying Code system where the skeptical consumer checks even the proofs of the typing rules. The model allows us to p......
#Logic #Object oriented modeling #Safety #Data structures #Java #Arithmetic #Computer languages #Computer science
Polarized games
Proceedings - Symposium on Logic in Computer Science - - Trang 265-274
We generalize the intuitionistic Hyland-Ong games to a notion of polarized games allowing games with plays starting by proponent moves. The usual constructions on games are adjusted to fit this setting yielding a game model for polarized linear logic with a definability result. As a consequence this gives a complete game model for various classical systems: LC, /spl lambda//spl mu/-calculus,... fo......
#Polarization #Logic programming #Computer languages #Waste materials #Computer science #Embedded computing
Some results on automatic structures
Proceedings - Symposium on Logic in Computer Science - - Trang 235-242
We study the class of countable structures which can be presented by synchronous finite automata. We reduce the problem of existence of an automatic presentation of a structure to that for a graph. We exhibit a series of properties of automatic equivalence structures, linearly ordered sets and permutation structures. These serve as a first step in producing practical descriptions of some automatic......
#Automata #Computer science #Mathematics #Terminology #Automatic logic units #Polynomials
Tổng số: 42
- 1
- 2
- 3
- 4
- 5