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)
Phân tích ảnh hưởng
Các bài báo tiêu biểu
A stratified semantics of general references embeddable in higher-order logic
- 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
The proof complexity of linear algebra
- 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
Some results on automatic structures
- 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
Efficient type inference for record concatenation and subtyping
- Trang 125-136
Record concatenation, multiple inheritance, and multiple-object cloning are closely related and part of various language designs. For example, in Cardelli's untyped Obliq language, a new object can be constructed from several existing objects by cloning followed by concatenation; an error is given in case of field name conflicts. Type systems for record concatenation have been studied by M. Wand (......
#Cloning #Concatenated codes #Computer science #Polynomials #Runtime #Calculus #Inference algorithms #Logic
Semantic minimization of 3-valued propositional formulae
- Trang 40-51
This paper presents an algorithm for a non-standard logic-minimization problem that arises in 3-valued propositional logic. The problem is motivated by the potential for obtaining better answers in applications that use 3-valued logic. An answer of 0 or 1 provides precise (definite) information; an answer of 1/2 provides imprecise (indefinite) information. By replacing a formula /spl phi/ with a "......
#Logic #Hardware #Data analysis #Information analysis #Software systems #Uncertainty #Contracts #Terminology #Minimization methods
A syntactic approach to foundational proof-carrying code
- Trang 89-100
Proof-carrying code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules. In foundational proof-carrying code (FPCC), on the other hand, proofs are constructed and verified using strictly the foundations of mathematical logic, with no type-specific axioms. FPCC is more f......
#Logic #Safety #Computer science #Buildings #Assembly systems #Computer bugs #Proposals
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
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
Complete problems for dynamic complexity classes
- Trang 313-322
We present the first complete problems for dynamic complexity classes including the classes Dyn-FO and Dyn-ThC/sup 0/, the dynamic classes corresponding to relational calculus and (polynomially bounded) SQL, respectively. The first problem we show complete for Dyn-FO is a single-step version of the circuit value problem (SSCV). Of independent interest, our construction also produces a first-order ......
#Polynomials #Computer science #Complexity theory #Databases #Heuristic algorithms #Data structures #Logic #Calculus #Circuits #Application software
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 ......
#Logic #Computer science #Switches #Art #Intelligent networks #Computer networks #Debugging #Contracts #Government