Explicit representation of terms defined by counter examples

From MaRDI portal
Publication:1100924

DOI10.1007/BF00243794zbMath0641.68124OpenAlexW3020128627MaRDI QIDQ1100924

Jean-Louis Lassez, Kim Marriott

Publication date: 1987

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00243794



Related Items

The DNF exception problem, Computing linearizations using test sets, Equational formulas and pattern operations in initial order-sorted algebras, On relationship between term rewriting systems and regular tree languages, Open problems in rewriting, The negation elimination from syntactic equational formula is decidable, More problems in rewriting, Sufficient-completeness, ground-reducibility and their complexity, Equational problems and disunification, On inductive inference of cyclic structures, Negation elimination in equational formulae, αCheck: A mechanized metatheory model checker, Extracting models from clause sets saturated under semantic refinements of the resolution rule., On the complexity of equational problems in CNF, NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment, First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation, Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning, Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria, A Transformational Approach to Prove Outermost Termination Automatically, Anti-patterns for rule-based languages, AC complement problems: Satisfiability and negation elimination, Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras, On deciding subsumption problems, Decidability Results for Saturation-Based Model Building, Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness, Classes of Tree Homomorphisms with Decidable Preservation of Regularity, Explicit versus implicit representations of subsets of the Herbrand universe., Working with ARMs: Complexity results on atomic representations of Herbrand models