Specification and proof in membership equational logic (Q1978640): Difference between revisions

@@ Property / describes a project that uses @@
+NQTHM
@@ Property / describes a project that uses: NQTHM / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing structural induction. II: Strategies
@@ Property / cites work: Mechanizing structural induction. II: Strategies / rank @@
+Normal rank
@@ Property / cites work @@
+Q3682648
@@ Property / cites work: Q3682648 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3896478
@@ Property / cites work: Q3896478 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264712
@@ Property / cites work: Q4264712 / rank @@
+Normal rank
@@ Property / cites work @@
+Using induction and rewriting to verify and complete parameterized specifications
+Normal rank
@@ Property / cites work @@
+Automated theorem proving by test set induction
@@ Property / cites work: Automated theorem proving by test set induction / rank @@
+Normal rank
@@ Property / cites work @@
+Automata-driven automated induction
@@ Property / cites work: Automata-driven automated induction / rank @@
+Normal rank
@@ Property / cites work @@
+Specification and proof in membership equational logic
+Normal rank
@@ Property / cites work @@
+Implicit induction in conditional theories
@@ Property / cites work: Implicit induction in conditional theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q3835049
@@ Property / cites work: Q3835049 / rank @@
+Normal rank
@@ Property / cites work @@
+Partial algebras-survey of a unifying approach towards a two-valued model theory for partial algebras
+Normal rank
@@ Property / cites work @@
+Pumping, cleaning and symbolic constraints solving
+Normal rank
@@ Property / cites work @@
+Encompassment properties and automata with constraints
+Normal rank
@@ Property / cites work @@
+May I borrow your logic? (Transporting logical structures along maps)
+Normal rank
@@ Property / cites work @@
+Q3785921
@@ Property / cites work: Q3785921 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3490949
@@ Property / cites work: Q3490949 / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive proofs by specification transformations
@@ Property / cites work: Inductive proofs by specification transformations / rank @@
+Normal rank
@@ Property / cites work @@
+Completion of rewrite systems with membership constraints. I: Deduction rules
+Normal rank
@@ Property / cites work @@
+Equational formulae with membership constraints
@@ Property / cites work: Equational formulae with membership constraints / rank @@
+Normal rank
@@ Property / cites work @@
+Q4942651
@@ Property / cites work: Q4942651 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3855354
@@ Property / cites work: Q3855354 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4385532
@@ Property / cites work: Q4385532 / rank @@
+Normal rank
@@ Property / cites work @@
+A rationale for conditional equational programming
+Normal rank
@@ Property / cites work @@
+Q3817652
@@ Property / cites work: Q3817652 / rank @@
+Normal rank
@@ Property / cites work @@
+Ground reducibility is EXPTIME-complete
@@ Property / cites work: Ground reducibility is EXPTIME-complete / rank @@
+Normal rank
@@ Property / cites work @@
+A strong restriction of the inductive completion procedure
+Normal rank
@@ Property / cites work @@
+Lokal präsentierbare Kategorien. (Locally presentable categories)
+Normal rank
@@ Property / cites work @@
+Reductions in tree replacement systems
@@ Property / cites work: Reductions in tree replacement systems / rank @@
+Normal rank
@@ Property / cites work @@
+A completion procedure for conditional equations
@@ Property / cites work: A completion procedure for conditional equations / rank @@
+Normal rank
@@ Property / cites work @@
+Order-sorted completion: The many-sorted way
@@ Property / cites work: Order-sorted completion: The many-sorted way / rank @@
+Normal rank
@@ Property / cites work @@
+Equational completion in order-sorted algebras
@@ Property / cites work: Equational completion in order-sorted algebras / rank @@
+Normal rank
@@ Property / cites work @@
+Q3719824
@@ Property / cites work: Q3719824 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3030249
@@ Property / cites work: Q3030249 / rank @@
+Normal rank
@@ Property / cites work @@
+Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
+Normal rank
@@ Property / cites work @@
+Abstract data types and software validation
@@ Property / cites work: Abstract data types and software validation / rank @@
+Normal rank
@@ Property / cites work @@
+The algebraic specification of abstract data types
+Normal rank
@@ Property / cites work @@
+Dynamically typed computations for order-sorted equational presentations
+Normal rank
@@ Property / cites work @@
+Proofs by induction in equational theories with constructors
+Normal rank
@@ Property / cites work @@
+Q3883561
@@ Property / cites work: Q3883561 / rank @@
+Normal rank
@@ Property / cites work @@
+Completion of a Set of Rules Modulo a Set of Equations
+Normal rank
@@ Property / cites work @@
+Q4297316
@@ Property / cites work: Q4297316 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming with equalities, subsorts, overloading, and parametrization in OBJ
+Normal rank
@@ Property / cites work @@
+Automatic proofs by induction in theories without constructors
+Normal rank
@@ Property / cites work @@
+Abstract data type systems
@@ Property / cites work: Abstract data type systems / rank @@
+Normal rank
@@ Property / cites work @@
+Conditional rewrite rules
@@ Property / cites work: Conditional rewrite rules / rank @@
+Normal rank
@@ Property / cites work @@
+Q3795207
@@ Property / cites work: Q3795207 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3338226
@@ Property / cites work: Q3338226 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3690200
@@ Property / cites work: Q3690200 / rank @@
+Normal rank
@@ Property / cites work @@
+Detecting redundant narrowing derivations by the LSE-SL reducibility test
+Normal rank
@@ Property / cites work @@
+Tree automata help one to solve equational formulae in AC-theories
+Normal rank
@@ Property / cites work @@
+Q4222853
@@ Property / cites work: Q4222853 / rank @@
+Normal rank
@@ Property / cites work @@
+Equational type logic
@@ Property / cites work: Equational type logic / rank @@
+Normal rank
@@ Property / cites work @@
+Inclusions and subtypes I: first-order case
@@ Property / cites work: Inclusions and subtypes I: first-order case / rank @@
+Normal rank
@@ Property / cites work @@
+Inclusions and subtypes II: higher-order case
@@ Property / cites work: Inclusions and subtypes II: higher-order case / rank @@
+Normal rank
@@ Property / cites work @@
+Q3032225
@@ Property / cites work: Q3032225 / rank @@
+Normal rank
@@ Property / cites work @@
+Conditional rewriting logic as a unified model of concurrency
+Normal rank
@@ Property / cites work @@
+Q3839051
@@ Property / cites work: Q3839051 / rank @@
+Normal rank
@@ Property / cites work @@
+Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
+Normal rank
@@ Property / cites work @@
+Q3204056
@@ Property / cites work: Q3204056 / rank @@
+Normal rank
@@ Property / cites work @@
+Parametrization for order-sorted algebraic specification
+Normal rank