Proceedings - Symposium on Logic in Computer Science
SCOPUS (1986-1987,1990-2011,2013,2015-2019,2021-2024)
1043-6871
Mỹ
Cơ quản chủ quản: Institute of Electrical and Electronics Engineers Inc.
Lĩnh vực:
SoftwareMathematics (miscellaneous)
Phân tích ảnh hưởng
Các bài báo tiêu biểu
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...
#Equations #Digital arithmetic #Educational institutions #Computer languages #Calculus #Logic programming #Functional programming #Algebra #Laboratories #Libraries
Author index
- Trang 457-457 - 2002
The author index contains an entry for each author and coauthor included in the
proceedings record.
Expressive equivalence of least and inflationary fixed-point logic
- Trang 403-410
We study the relationship between least and inflationary fixed-point logic. By
results of Gurevich and Shelah (1986), it has been known that on finite
structures both logics have the same expressive power. On infinite structures
however the question whether there is a formula in IFP not equivalent to any
LFP-formula was still open. In this paper, we settle the question by showing
that both logics ...
#Logic #Relational databases #Polynomials #Computer science #History #Arithmetic #Database languages #Calculus #Computational complexity #Artificial intelligence
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...
#Encoding #Computational complexity #Polynomials #Calculus #Logic #Computer science
Little engines of proof
- Trang 3
Summary form only given. The automated construction of mathematical proof is a
basic activity in computing. Since the dawn of the field of automated reasoning,
there have been two divergent schools of thought. One school, best represented
by Alan Robinson's resolution method, is based on simple uniform proof search
procedures guided by heuristics. The other school, pioneered by Hao Wang, argues
fo...
#Engines #Educational institutions #Computer science #Contracts #Laboratories #Uniform resource locators #Decision feedback equalizers #Arithmetic #NASA #Europe
Tree extension algebras: logics, automata, and query languages
- Trang 203-212
We study relations on trees defined by first-order constraints over a vocabulary
that includes the tree extension relation T...
#Algebra #Logic functions #Automata #Database languages #XML #Query processing #Logic programming #Computer science #Transducers #Vocabulary
Semantic subtyping
- Trang 137-146
Usually subtyping relations are defined either syntactically by a formal system
or semantically by an interpretation of types in an untyped denotational model.
In this paper we show how to define a subtyping relation semantically, for a
language whose operational semantics is driven by types; we consider a rich type
algebra, with product, arrow, recursive, intersection, union and complement
types....
#Algebra #XML #Programming profession #Databases
The complexity of first-order and monadic second-order logic revisited
- Trang 215-224
The model-checking problem for a logic L on a class C of structures asks whether
a given L-sentence holds in a given structure in C. In this paper, we give
super-exponential lower bounds for fixed-parameter tractable model-checking
problems for first-order and monadic second-order logic. We show that unless
PTIME=NP, the model-checking problem for monadic second-order logic on finite
words is not ...
#Logic #Complexity theory #Polynomials #Databases #Computer science #Informatics #Upper bound #Artificial intelligence #State-space methods
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
...
#Data structures #Computer science #Programmable logic arrays #Reflection #Logic programming #Computer languages #Logic arrays #Arithmetic #Artificial intelligence #Bibliographies
Monadic queries over tree-structured data
- Trang 189-202
Monadic query languages over trees currently receive considerable interest in
the database community, as the problem of selecting nodes from a tree is the
most basic and widespread database query problem in the context of XML. Partly a
survey of recent work done by the authors and their group on logical query
languages for this problem and their expressiveness, this paper provides a
number of new ...
#Database languages #XML #Logic #Data mining #Wrapping #Artificial intelligence #Natural languages #Spatial databases #Information filtering #Information filters