Switch to: References

Citations of:

Refutational theorem proving using term-rewriting systems

Jieh Hsiang

Artificial Intelligence 25 (3):255-300 (1985)

Add citations

You must login to add citations.

Polynomial ring calculus for modal logics: A new semantics and proof method for modalities: Polynomial ring calculus for modal logics.Juan C. Agudelo - 2011 - Review of Symbolic Logic 4 (1):150-170.details A new proof style adequate for modal logics is defined from the polynomial ring calculus. The new semantics not only expresses truth conditions of modal formulas by means of polynomials, but also permits to perform deductions through polynomial handling. This paper also investigates relationships among the PRC here defined, the algebraic semantics for modal logics, equational logics, the Dijkstra???Scholten equational-proof style, and rewriting systems. The method proposed is throughly exemplified for S 5, and can be easily extended to other modal (...) logics. (shrink) Download Export citation Bookmark 3 citations
CWA Extensions to Multi-Valued Logics.Jinzhao Wu - 2003 - Journal of Applied Non-Classical Logics 13 (2):133-164.details The closed world assumption plays a fundamental role in the theory of deductive databases. On the other hand, multi-valued logics occupy a vast field in non-classical logics. Some questions are better explained and expressed in terms of such logics. To enhance the expressive power and the declarative ability of a deductive database, we extend various CWA formalizations, including the naive CWA, the generalized CWA and the careful CWA, to multi-valued logics. The basic idea is to embed logic formulae into some (...) Download Export citation Bookmark
On Theorem Proving in Annotated Logics.Mi Lu & Jinzhao Wu - 2000 - Journal of Applied Non-Classical Logics 10 (2):121-143.details ABSTRACT We are concerned with the theorem proving in annotated logics. By using annotated polynomials to express knowledge, we develop an inference rule superposition. A proof procedure is thus presented, and an improvement named M- strategy is mainly described. This proof procedure uses single overlaps instead of multiple overlaps, and above all, both the proof procedure and M-strategy are refutationally complete. Download Export citation Bookmark
An Algebraic Method to Decide the Deduction Problem in Many-Valued Logics.Jinzhao Wu, Hongyan Tan & Yongli Li - 1998 - Journal of Applied Non-Classical Logics 8 (4):353-360.details ABSTRACT We show that there is a polynomial over the rational number field corresponding to each propositional formula in a given many-valued logic. To decide whether a propositional formula can be deduced from a finite set of such formulas (deduction problem), we only need to decide whether a polynomial vanishes on an algebraic variety. By using Wu's method, an algorithm for this problem is presented. Download Export citation Bookmark 2 citations
Modular algebraic specification of some basic geometrical constructions.Joseph A. Goguen - 1988 - Artificial Intelligence 37 (1-3):123-153.details Download Export citation Bookmark 2 citations
A multi-level geometric reasoning system for vision.Michele Barry, David Cyrluk, Deepak Kapur, Joseph Mundy & Van-Duc Nguyen - 1988 - Artificial Intelligence 37 (1-3):291-332.details Download Export citation Bookmark

1