scientific article; zbMATH DE number 599028
From MaRDI portal
Publication:4297316
zbMath0793.03002MaRDI QIDQ4297316
No author found.
Publication date: 3 July 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Proceedings, conferences, collections, etc. pertaining to computer science (68-06) Festschriften (00B30) Mechanization of proofs and logical operations (03B35) Logic programming (68N17) Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations (03-06) Combinatory logic and lambda calculus (03B40)
Related Items (79)
A resolution principle for constrained logics ⋮ Unfold/fold transformations for disjunctive logic programs ⋮ Semi-unification of two terms in Abelian groups ⋮ Constructor equivalent term rewriting systems are strongly sequential: A direct proof ⋮ Rules + strategies for transforming lazy functional logic programs ⋮ Strongly sequential and inductively sequential term rewriting systems ⋮ Compiling a Functional Logic Language: The Fair Scheme ⋮ Higher-order families ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ Improving the Efficiency of Non-Deterministic Computations1 1Supported in part by NSF grants INT-9981317 and CCR-0110496 and by the Spanish Knowledge Society Foundation, the Spanish Research Funding Agency (CICYT) TIC 2001-2705-C03-01, by Acción Integrade Hispano-Italiana HI2000-0161, and the Valencian Research Council under grant GV01-424. ⋮ Higher-order rewrite systems and their confluence ⋮ On First-Order Model-Based Reasoning ⋮ Lazy narrowing: Strong completeness and eager variable elimination (extended abstract) ⋮ Abstract data type systems ⋮ Unification of infinite sets of terms schematized by primal grammars ⋮ Unification of drags and confluence of drag rewriting ⋮ Extracting models from clause sets saturated under semantic refinements of the resolution rule. ⋮ Jean van Heijenoort's contributions to proof theory and its history ⋮ Towards Ontology Evolution in Physics ⋮ A pearl on SAT and SMT solving in Prolog ⋮ A Needed Rewriting Strategy for Data-Structures with Pointers ⋮ On Normalisation of Infinitary Combinatory Reduction Systems ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ On solving nominal disunification constraints ⋮ Termination of just/fair computations in term rewriting ⋮ Theorem proving modulo ⋮ Evaluation strategies for functional logic programming ⋮ Specification and proof in membership equational logic ⋮ Sequentiality in orthogonal term rewriting systems ⋮ Lazy narrowing: strong completeness and eager variable elimination ⋮ Combination techniques and decision problems for disunification ⋮ A combinatory logic approach to higher-order E-unification ⋮ Development closed critical pairs ⋮ A method for simultaneous search for refutations and models by equational constraint solving ⋮ Complete axiomatizations of some quotient term algebras ⋮ An algebraic semantics for structured transition systems and its application to logic programs ⋮ AC-unification race: The system solving approach, implementation and benchmarks ⋮ Constructor equivalent term rewriting systems ⋮ Optimizing Fuzzy Logic Programs by Unfolding, Aggregation and Folding ⋮ A transformation system for deductive database modules with perfect model semantics ⋮ Categorical rewriting of term-like structures ⋮ Decidable call-by-need computations in term rewriting ⋮ Anti-patterns for rule-based languages ⋮ Strictly orthogonal left linear rewrite systems and primitive recursion ⋮ Automata-driven efficient subterm unification ⋮ Normalisation for higher-order calculi with explicit substitutions ⋮ A Single-Significant-Digit Calculus for Semi-Automated Guesstimation ⋮ Type inference with simple subtypes ⋮ On the longest perpetual reductions in orthogonal expression reduction systems ⋮ Foundations of Refinement Operators for Description Logics ⋮ Relating graph and term rewriting via Böhm models ⋮ Semantics and strong sequentiality of priority term rewriting systems ⋮ Strong and NV-sequentiality of constructor systems ⋮ Evaluation Strategies for Functional Logic Programming ⋮ Lazy Rewriting and Context-Sensitive Rewriting ⋮ Proof-search in type-theoretic languages: An introduction ⋮ A symbolic decision procedure for cryptographic protocols with time stamps ⋮ Source-tracking unification ⋮ Automating Signature Evolution in Logical Theories ⋮ Normalization, approximation, and semantics for combinator systems ⋮ Semi-explicit first-class polymorphism for ML. ⋮ Bisimilarity in term graph rewriting. ⋮ Sequentiality, monadic second-order logic and tree automata. ⋮ Higher order unification via explicit substitutions ⋮ Descendants and origins in term rewriting. ⋮ Induction = I-axiomatization + first-order consistency. ⋮ Unification algorithms cannot be combined in polynomial time. ⋮ Perpetuality and uniform normalization in orthogonal rewrite systems ⋮ Naming and identity in epistemic logic. II: A first-order logic for naming ⋮ The conflict-free reduction geometry ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Lazy Context Cloning for Non-Deterministic Graph Rewriting ⋮ Relating conflict-free stable transition and event models via redex families ⋮ Comparing logics for rewriting: Rewriting logic, action calculi and tile logic ⋮ Unification in free distributive lattices ⋮ Origin tracking ⋮ Logical debugging ⋮ Mathematics based on incremental learning -- excluded middle and inductive inference
This page was built for publication:
