Resolution, inverse method and the sequent calculus

MaRDI QIDQ4364504zbMATH OpenFDO

Authors Tanel Tammet

Publication date 17 November 1997

zbMATH Keywords

automated deductionproof theoryresolution calculi for non-classical logicsresolution-based decision methodsurvey

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)

Review text

A survey of resolution calculi for various non-classical logics is presented and a resolution-based decision method for a new (Near-Monadic) class is sketched. For the entire collection see [Zbl 0870.00023].

Cited in

(6)

• scientific article; zbMATH DE number 77919 (Why is no real title available?)
• scientific article; zbMATH DE number 517062 (Why is no real title available?)
• The ILLTP library for intuitionistic linear logic
• From modal sequent calculi to modal resolution
• A logical characterization of forward and backward chaining in the inverse method
• Resolution is cut-free

This page was built for publication: Resolution, inverse method and the sequent calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4364504)