scientific article; zbMATH DE number 3684925
From MaRDI portal
Publication:3880309
Cited in
(45)- Inductive proof search modulo
- Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories
- Some fundamental algebraic tools for the semantics of computation: II. Signed and abstract theories
- A superposition oriented theorem prover
- On sufficient-completeness and related properties of term rewriting systems
- Proof by consistency
- Rewriting with a nondeterministic choice operator
- Equivalences and transformations of regular systems - applications to recursive program schemes and grammars
- Simplifying conditional term rewriting systems: Unification, termination and confluence
- History and basic features of the critical-pair/completion procedure
- Automatic inductive theorem proving using Prolog
- Modular algebraic specification of some basic geometrical constructions
- Algebraic implementation of abstract data types
- Conditional rewriting logic as a unified model of concurrency
- Paramorphisms
- Schematization of infinite sets of rewrite rules generated by divergent completion processes
- The equational part of proofs by structural induction
- Gordon's computer: A hardware verification case study in OBJ3
- A strong restriction of the inductive completion procedure
- Automatic proofs by induction in theories without constructors
- Induction using term orders
- Sufficient-completeness, ground-reducibility and their complexity
- Obtaining contradiction measures on intuitionistic fuzzy sets from fuzzy connectives
- Comparing data type specifications via their normal forms
- Inductive proofs by specification transformations
- Proving and rewriting
- Induction using term orderings
- On the connection between narrowing and proof by consistency
- Order-sorted unification
- Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
- Conditional rewriting logic: Deduction, models and concurrency
- Proof by consistency in conditional equational theories
- Completion procedures as semidecision procedures
- Term rewriting induction
- UNICOM: A refined completion based inductive theorem prover
- Semantics of non-terminating rewrite systems using minimal coverings
- Higher-order proof by consistency
- Transformations and confluence for rewrite systems
- Towards a foundation of completion procedures as semidecision procedures
- A unified view of induction reasoning for first-order logic
- Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
- NuITP: accelerating the inductive verification of equational programs through symbolic simplification
- Automating inductionless induction using test sets
- Proofs by induction in equational theories with constructors
- Algebraic specification of concurrent systems
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3880309)
