scientific article

No author found.

Publication date: 23 January 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Computer science Logic term rewriting systems theorem provers lambda calculi Computational structures modal and temporal logics algorithmic logics

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science (68-00) Combinatory logic and lambda calculus (03B40) Thue and Post systems, etc. (03D03)

Related Items

Metric axioms and distance, Level-confluence of conditional rewrite systems with extra variables in right-hand sides, Higher-order families, Automath Type Inclusion in Barendregt’s Cube, Unnamed Item, A Debugging Scheme for Functional Logic Programs1 1This work has been partially supported by CICYT under grant TIC2001-2705-C03-01, by Acción Integrada Hispano-Italiana HI2000-0161, Acción Integrada Hispano-Alemana HA2001-0059 and by Generalitat Valenciana under grant GV01-424., On K-modal BL-logics, Refinement by Interpretation in a General Setting, A Type Theory for Probabilistic $$\lambda $$–calculus, Algebraic Methods for Rough Approximation Spaces by Lattice Interior–Closure Operations, A new generalization of contra-continuity via Levine's $g$-closed sets, Development closed critical pairs, Transforming termination by self-labelling, A Branching Time Logical System for Open Distributed Systems Development, Modal Operators for Coequations, An Automata-Theoretic Approach to the Reachability Analysis of RPPS Systems, A solution of the word problem for free $^*$-regular semigroups, Symbolic protocol analysis for monoidal equational theories, Admissible Representations of Probability Measures, On Computable Metrization, Visual Modeling of Distributed Object Systems by Graph Transformation, Automath and Pure Type Systems, On the semantics of classical disjunction, On modularity in infinitary term rewriting, Investigations on the dual calculus, Intrinsic reasoning about functional programs. I: First order theories, Inductive-data-type systems, Distributed processes and location failures, An induction principle for pure type systems, Type inference for set theory, Unnamed Item, Shallow confluence of conditional term rewriting systems, Simple termination revisited, Extending set functors to generalised metric spaces, Declarative Debugging of Functional Logic Programs1 1This work has been partially supported by CICYT under grant TIC2001-2705-C03-01, by Accóon Integrada Hispano-Italiana HI2000-0161 and by Generalitat Valenciana under grant GV01-424., Containers: Constructing strictly positive types, An axiomatization of PCTL*, Probabilistic temporal logics via the modal mu-calculus, An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types, Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I, Structure and Properties of Traces for Functional Programs, Inductive and Coinductive Components of Corecursive Functions in Coq, Probabilistic Temporal Logics, A rewriting coherence theorem with applications in homotopy type theory, Finding direct partition bijections by two-directional rewriting techniques, Nominal unification, The Church-Rosser theorem and quantitative analysis of witnesses, Variants of the basic calculus of constructions, Intersection types for explicit substitutions, A complete equational axiomatization for prefix iteration, Semantics of a sequential language for exact real-number computation, Ultraproducts and possible worlds semantics in institutions, Recursively defined metric spaces without contraction, The data type variety of stack algebras, On modal mu-calculus and Büchi tree automata, PCF extended with real numbers, Fast and simple nested fixpoints, Strong normalization for non-structural subtyping via saturated sets, Constructing a quasi-uniform function space, On confluence and residuals in Cauchy convergent transfinite rewriting, A duality for two-sorted lattices, A logical approach to stable domains, A formal fuzzy reasoning system and reasoning mechanism based on propositional modal logic, Preferential choice and coordination conditions, Innovations in computational type theory using Nuprl, Partial Horn logic and Cartesian categories, Towards the hierarchical verification of reactive systems, The decidability of a fragment of $\text{BB}'\text{IW}$-logic, Partial arithmetical data types of rational numbers and their equational specification, Strong normalisation in the $\pi$-calculus, Higher-order rewrite systems and their confluence, The two-way rewriting in action: removing the mystery of Euler-Glaisher's map, Infinitary rewriting: meta-theory and convergence, A scalable module system, Axiomatising extended computation tree logic, Computing in unpredictable environments: semantics, reduction strategies, and program transformations, Possibilistic reasoning -- a mini-survey and uniform semantics, Developing developments, Independent subbases and non-redundant codings of separable metrizable spaces, Some topological notations via Maki's $\Lambda $-sets, Revisiting the notion of function, On $\Lambda_{\alpha}$-sets and the associated topology $T^{\Lambda_\alpha}$, Termination of rewrite relations on $\lambda$-terms based on Girard's notion of reducibility, Proof theory of higher-order equations: Conservativity, normal forms and term rewriting., Algebraic models of deviant modal operators based on De Morgan and Kleene lattices, On intuitionistic modal and tense logics and their classical companion logics: topological semantics and bisimulations, Coalgebras in functional programming and type theory, Mathematical modal logic: A view of its evolution, Program schemata technique for propositional program logics: a 30-year history, Algebraic models of correctness for abstract pipelines., Termination of just/fair computations in term rewriting, Ideal models of spaces., Some points in formal topology., Exploring conditional rewriting logic computations, Termination of term rewriting using dependency pairs, Logicality of conditional rewrite systems, Algebraic models of behaviour and correctness of SMT and CMT processors, Primitive recursive selection functions for existential assertions over abstract algebras, A compositional semantic basis for the analysis of equational Horn programs, Elements of generalized ultrametric domain theory, A hierarchy of temporal logics with past, Natural termination, Translations between modal logics of reactive systems, Termination is not modular for confluent variable-preserving term rewriting systems, A Henneberg-based algorithm for generating tree-decomposable minimally rigid graphs, On $(LC, s)$-continuous functions, De Bruijn's syntax and reductional behaviour of $\lambda$-terms: the untyped case, The probabilistic powerdomain for stably compact spaces, On the completeness and decidability of duration calculus with iteration, A compact fixpoint semantics for term rewriting systems, Debugging Maude programs via runtime assertion checking and trace slicing, Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician, N. G. de Bruijn's contribution to the formalization of mathematics, Generating priority rewrite systems for OSOS process languages, Topology on words, Applications of infinitary lambda calculus, How to win a game with features, Explicit substitution. On the edge of strong normalization, Induction and recursion on the partial real line with applications to Real PCF, Structural induction and coinduction in a fibrational setting, Two-level languages for program optimization, Order-sorted inductive types, Perpetual reductions in $\lambda$-calculus, Some characteristics of strong innermost normalization, Swinging types=functions+relations+transition systems, Symbolic model checking for $\mu$-calculus requires exponential time, On the intuitionistic force of classical search, Proof-search in type-theoretic languages: An introduction, Properly injective spaces and function spaces, On principal types of combinators, Universal coalgebra: A theory of systems, Formalization of universal algebra in Agda, Decidable fragments of first-order temporal logics, A category of compositional domain-models for separable Stone spaces., Normalization, approximation, and semantics for combinator systems, The combinator S, Modular termination proofs for rewriting using dependency pairs, On the Yoneda completion of a quasi-metric space, Soundness of data refinement for a higher-order imperative language, A new way to extend t-norms, t-conorms and negations, Real number computation through Gray code embedding., Relating conflict-free stable transition and event models via redex families, Generated quasi-metric hyper and function spaces., Syntactic control of concurrency

Uses Software