Proceedings - Symposium on Logic in Computer Science
SCOPUS (1986-1987,1990-2011,2013,2015-2019,2021-2023)
1043-6871
Mỹ
Cơ quản chủ quản: Institute of Electrical and Electronics Engineers Inc.
Lĩnh vực:
SoftwareMathematics (miscellaneous)
Các bài báo tiêu biểu
Tree-like counterexamples in model checking
- Trang 19-29
Counter examples for specification violations provide engineers with important debugging information. Although counterexamples are considered one of the main advantages of model checking, state-of the art model checkers are restricted to relatively simple counterexamples, and surprisingly little research effort has been put into counterexamples. In this paper, we introduce a new general framework ...... hiện toàn bộ
#Logic #Computer science #Switches #Art #Intelligent networks #Computer networks #Debugging #Contracts #Government
Semantics and logic of object calculi
- Trang 113-122
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
Temporal logic with forgettable past
- Trang 383-392
We investigate NLTL, a linear-time temporal logic with forgettable past. NLTL can be exponentially more succinct than LTL+Past (which in turn can be more succinct than LTL). We study satisfiability and model checking for NLTL and provide optimal automata-theoretic algorithms for these EXPSPACE-complete problems.
#Automatic logic units #Computer science #Polynomials
Logic phân tách: một logic cho cấu trúc dữ liệu có thể biến đổi chia sẻ Dịch bởi AI
- Trang 55-74
Trong công trình hợp tác với Peter O'Hearn và những người khác, dựa trên những ý tưởng ban đầu của Burstall, chúng tôi đã phát triển một mở rộng của logic Hoare cho phép lập luận về các chương trình lệnh cấp thấp sử dụng cấu trúc dữ liệu có thể thay đổi được chia sẻ. Ngôn ngữ lập trình lệnh đơn giản được mở rộng với các lệnh (không phải biểu thức) để truy cập và sửa đổi các cấu trúc chia sẻ, cũng ...... hiện toàn bộ
#Data structures #Computer science #Programmable logic arrays #Reflection #Logic programming #Computer languages #Logic arrays #Arithmetic #Artificial intelligence #Bibliographies
Modal and guarded characterisation theorems over finite transition systems
- 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...... hiện toàn bộ
#Logic #H infinity control #Game theory #Computer science
Proceedings 17th Annual IEEE Symposium on Logic in Computer Science
- 2002
Presents the front cover of the proceedings record.
Unsatisfiable random formulas are hard to certify
- 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...... hiện toàn bộ
#Encoding #Computational complexity #Polynomials #Calculus #Logic #Computer science
Separability, expressiveness, and decidability in the ambient logic
- Trang 423-432
The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. We study some basic questions concerning the descriptive and discriminating power of AL, focusing on the equivalence on processes induced by the logic (=/sub L/). We consider MA, and two Turing complete subsets of...... hiện toàn bộ
#Logic #Chromium #Calculus #Database languages #Switches #Computer science #Query processing #Shape
Remarks on isomorphisms in typed lambda calculi with empty and sum types
- Trang 147-156
Tarski asked whether the arithmetic identities taught in high school are complete for showing all arithmetic equations valid for the natural numbers. The answer to this question for the language of arithmetic expressions using a constant for the number one and the operations of product and exponentiation is affirmative, and the complete equational theory also characterises isomorphism in the typed...... hiện toàn bộ
#Equations #Digital arithmetic #Educational institutions #Computer languages #Calculus #Logic programming #Functional programming #Algebra #Laboratories #Libraries
On the lambda Y calculus
- 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...... hiện toàn bộ
#Calculus #Magnetic heads #Encoding #Equations #Logic #Computer science #Standardization