scientific article

From MaRDI portal
Publication:2751360

zbMath1011.68126MaRDI QIDQ2751360

Wayne Snyder, Franz Baader

Publication date: 27 August 2002


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



Related Items

Admissibility and unification in the modal logics related to S4.2, Inferring region types via an abstract notion of environment transformation, On rules, About the unification type of modal logics between \(\mathbf{KB}\) and \(\mathbf{KTB} \), Non-disjoint combined unification and closure by equational paramodulation, Deciding unifiability and computing local unifiers in the description logic \(\mathcal{EL}\) without top constructor, UNIFICATION IN INTERMEDIATE LOGICS, The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem, Typed Relational Conversion, Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, An efficient labelled nested multiset unification algorithm, Code-carrying theories, Fast algorithms for uniform semi-unification, A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties, Unnamed Item, Representing and building models for decidable subclasses of equational clausal logic, Some techniques for proving termination of the hyperresolution calculus, Multiagent temporal logics, unification problems, and admissibilities, Nominal Unification and Matching of Higher Order Expressions with Recursive Let, Scheduling complexity of interleaving search, Multi-agent logics with dynamic accessibly relations, projective unifiers, A geometric interpretation of LD-resolution, Unification, finite duality and projectivity in varieties of Heyting algebras, E-Unification based on Generalized Embedding, Permutative rewriting and unification, Formal correctness of a quadratic unification algorithm, Tree tuple languages from the logic programming point of view, Finitary unification in locally tabular modal logics characterized, Unification and admissible rules for paraconsistent minimal Johanssons' logic J and positive intuitionistic logic \(\mathbf{IPC}^+\), GUBS a Language for Synthetic Biology: Specification and Compilation, Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis, On the Parameterized Complexity of Associative and Commutative Unification, A Certified Functional Nominal C-Unification Algorithm, Projectivity and unification in substructural logics of generalized rotations, Dynamic temporal logical operations in multi-agent logics, Taming strategy logic: non-recurrent fragments, Unification in varieties of completely regular semigroups, Nominal Matching and Alpha-Equivalence, Unification and Matching in Hierarchical Combinations of Syntactic Theories, A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, Cut elimination for a logic with induction and co-induction, Placement Inference for a Client-Server Calculus, Admissible rules in the implication-negation fragment of intuitionistic logic, An instantiation scheme for satisfiability modulo theories, \(E\)-unification with constants vs. general \(E\)-unification, Incremental preprocessing methods for use in BMC, Unnamed Item, Best unifiers in transitive modal logics, Unnamed Item, Anti-unification and the theory of semirings, Extensions of unification modulo ACUI, Bounded ACh unification, Superposition with completely built-in abelian groups, Solving equations with sequence variables and sequence functions, Exploring conditional rewriting logic computations, Commutative rational term rewriting, What Is Essential Unification?, Unification in pretabular extensions of S4, Intruder deduction problem for locally stable theories with normal forms and inverses, Proximity-based unification theory, Symbolic protocol analysis for monoidal equational theories, Termination of narrowing via termination of rewriting, The correctness of Newman's typability algorithm and some of its extensions, Variant Narrowing and Equational Unification, Herbrand's theorem and term induction, Tractable query answering and rewriting under description logic constraints, Essential unifiers, Matching and alpha-equivalence check for nominal terms, Variadic equational matching in associative and commutative theories, Efficient General Unification for XOR with Homomorphism, Unification and projectivity in De Morgan and Kleene algebras., On the parameterized complexity of associative and commutative unification, Flat matching, A partial evaluation framework for order-sorted equational programs modulo axioms, Debugging Maude programs via runtime assertion checking and trace slicing, Constructing orthogonal designs in powers of two via symbolic computation and rewriting techniques, Regular expression order-sorted unification and matching, Automated Verification of Equivalence Properties of Cryptographic Protocols, Equational theorem proving modulo, Unification modulo lists with reverse relation with certain word equations, Unification in the Description Logic $\mathcal{EL}$, Unification with Singleton Tree Grammars, Word Equations with One Unknown, Identity Problems, Solvability of Equations and Unification in Varieties of Semigroups Related to Varieties of Groups, Order-Sorted Generalization, Solving quantified verification conditions using satisfiability modulo theories, Syntactic Unification as a Geometric Operation in Free Modules over certain Rings, Context unification with one context variable, Rewriting Conjunctive Queries over Description Logic Knowledge Bases, α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic, A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs, A formalisation of nominal C-matching through unification with protected variables, Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK, Unification in Linear Modal Logic on Non-transitive Time with the Universal Modality, Distributive bilattices from the perspective of natural duality theory., Faster linear unification algorithm, Rules with parameters in modal logic. I., Formalising nominal C-unification generalised with protected variables, A complete superposition calculus for primal grammars, Symbolic computation in Maude: some tapas, Terminating non-disjoint combined unification