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:
Description logics: foundations for class-based knowledge representation
Proceedings - Symposium on Logic in Computer Science - - Trang 359-370
Class-based languages express knowledge in terms of objects and classes, and have inspired a huge number of formalisms in computer science. Description logics forma family of both class-based and logic-based knowledge representation languages which allow for modeling an application domain in terms of objects, classes and relationships between classes, and for reasoning about them. This paper prese...... hiện toàn bộ
#Knowledge representation #Computer science #Object oriented modeling #Application software #Logic programming #Computer languages #Object oriented databases #Software engineering #Remuneration #Specification languages
Separability, expressiveness, and decidability in the ambient logic
Proceedings - Symposium on Logic in Computer Science - - 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
Calibrating computational feasibility by abstraction rank
Proceedings - Symposium on Logic in Computer Science - - Trang 345-354
We characterize computationally the functions provable in second order logic with set existence restricted to natural classes of first order formulas. A classification of first-order set-existence by implicational rank yields a natural hierarchy of complexity classes within the class of Kalmar-elementary functions: The functions over {0, 1}* constructively provable using set existence for formulas...... hiện toàn bộ
#Equations #Arithmetic #Logic #Computational complexity #Mathematics #Mathematical programming #Reasoning about programs #Calculus #Calibration #Size control
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...... hiện toàn bộ
#Logic #H infinity control #Game theory #Computer science
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 ...... hiện toàn bộ
#Logic #Computer science #Educational institutions #Knowledge representation #Application software #Turning #History
Automatic decidability
Proceedings - Symposium on Logic in Computer Science - - Trang 7-16
We give a set of inference rules with constant constraints. Then we show how to extend a set of equational clauses, so that if the application of these inference rules halts on these clauses, then the theory is decidable by applying a standard set of Paramodulation inference rules. In addition, we can determine the number of clauses generated in this decision procedure. For some theories, such as ...... hiện toàn bộ
#Equations #Polynomials #Mathematics #Computer science #Application software #Data structures #Logic #Automation #Inference algorithms
The 0-1 law fails for frame satisfiability of propositional modal logic
Proceedings - Symposium on Logic in Computer Science - - Trang 225-234
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
A fully abstract may testing semantics for concurrent objects
Proceedings - Symposium on Logic in Computer Science - - Trang 101-112
This paper provides a fully abstract semantics for a variant of the concurrent object calculus. We define may testing for concurrent object components and then characterise it using a trace semantics inspired by UML interaction diagrams. The main result of this paper is to show that the trace semantics is fully abstract for may testing. This is the first such result for a concurrent object languag...... hiện toàn bộ
#Testing #Calculus #Unified modeling language #Yarn #Production facilities #Safety #Robustness #Visualization #Jacobian matrices #Standards development
The metric analogue of weak bisimulation for probabilistic processes
Proceedings - Symposium on Logic in Computer Science - - Trang 413-422
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
Tổng số: 42
- 1
- 2
- 3
- 4
- 5