Refutational theorem proving using term-rewriting systems
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3871322 (Why is no real title available?)
- scientific article; zbMATH DE number 3871334 (Why is no real title available?)
- scientific article; zbMATH DE number 3810909 (Why is no real title available?)
- scientific article; zbMATH DE number 3936507 (Why is no real title available?)
- scientific article; zbMATH DE number 3981150 (Why is no real title available?)
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 3550181 (Why is no real title available?)
- scientific article; zbMATH DE number 3566230 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3310921 (Why is no real title available?)
- scientific article; zbMATH DE number 3346109 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- scientific article; zbMATH DE number 3415409 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- A Unification Algorithm for Associative-Commutative Functions
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- A simplified problem reduction format
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Complete Sets of Reductions for Some Equational Theories
- Completion of a Set of Rules Modulo a Set of Equations
- Computer-Implemented Set Theory
- Experiment with an automatic theorem-prover having partial ordering inference rules
- New decision algorithms for finitely presented commutative semigroups
- Non-resolution theorem proving
- Orderings for term-rewriting systems
- Proving Theorems with the Modification Method
- Theorem-Proving on the Computer
Cited in
(66)- Revisiting four-valued logics from \textit{Maple} using the \textit{Logics Explorer} package
- Proving and rewriting
- scientific article; zbMATH DE number 2016837 (Why is no real title available?)
- The problem of demodulator adjunction
- Rewrite method for theorem proving in first order theory with equality
- A refutational approach to geometry theorem proving
- A logic-algebraic tool for reasoning with knowledge-based systems
- A Gröbner bases-based rule based expert system for fibromyalgia diagnosis
- An inference engine for propositional two-valued logic based on the radical membership problem
- Completion for rewriting modulo a congruence
- Conditional rewrite rule systems with built-in arithmetic and induction
- Open problems in rewriting
- Canonical ground Horn theories
- An algebraic model for implementing expert systems based on the knowledge of different experts
- Automatic inductive theorem proving using Prolog
- A prototype of a RBES for personalized menus generation
- A new algebraic model for implementing expert systems represented under the `concept-attribute-value' paradigm
- A natural language for implementing algebraically expert systems
- An algebraic approach for detecting nearly dangerous situations in expert systems
- Boolean algebra admits no convergent term rewriting system
- Modular algebraic specification of some basic geometrical constructions
- A Groebner Bases Based Many-Valued Modal Logic Implementation in Maple
- A logic-algebraic approach to decision taking in a railway interlocking system
- Towards automated deduction in cP systems
- Theorem proving by chain resolution
- Buchberger's algorithm: a constraint-based completion procedure
- Buchberger's algorithm: The term rewriter's point of view
- Ordered binary decision diagrams and the Davis-Putnam procedure
- On conversions from CNF to ANF
- Towards a foundation of completion procedures as semidecision procedures
- Use of logical models for proving infeasibility in term rewriting
- Refutational theorem proving for hierarchic first-order theories
- Could orders be captured by term rewriting systems?
- Multi-valued logic and Gröbner bases with applications to modal logic
- Discriminator varieties and symbolic computation
- An expert system for managing medical appropriateness criteria based on computer algebra techniques
- scientific article; zbMATH DE number 4074536 (Why is no real title available?)
- Termination orderings for associative-commutative rewriting systems
- Embedding Boolean expressions into logic programming
- Unification in Boolean rings
- Structures for abstract rewriting
- A Groebner bases-based approach to backward reasoning in rule based expert systems
- A polynomial model for logics with a prime power number of truth values
- Polynomial ring calculus for modal logics: a new semantics and proof method for modalities
- On the relation between resolution based and completion based theorem proving
- The Multi-SAT algorithm
- Gordon's computer: A hardware verification case study in OBJ3
- Boolean unification - the story so far
- The Logics' Explorer: a Maple package for exploring finite many-valued propositional logics
- Fuzzy term-rewriting system
- A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules
- On Theorem Proving in Annotated Logics
- CWA extensions to multi-valued logics
- An Algebraic Method to Decide the Deduction Problem in Many-Valued Logics
- Rewriting-based verification of authentication protocols
- Incremental techniques for efficient normalization of nonlinear rewrite systems
- Subsumption computed algebraically
- Critical pair criteria for completion
- Completion procedures as semidecision procedures
- Partial completion of equational theories
- scientific article; zbMATH DE number 3930371 (Why is no real title available?)
- Linear strategy for Boolean ring based theorem proving
- A portable knowledge-based system for car breakdown evaluation
- Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
- Incremental proofs of termination, confluence and sufficient completeness of OBJ specifications
- An algebraic approach to rule based expert systems
This page was built for publication: Refutational theorem proving using term-rewriting systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q802317)
