scientific article

zbMath0992.03015MaRDI QIDQ2751372

Gernot Salzer, Matthias Baaz, Christian G. Fermüller

Publication date: 5 September 2002

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

many-valued logicproof systemsautomated theorem provingresolution methodsigned logicsigned formulasmany-valued automated reasoning

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50)

Related Items

Analytic tableaux for non-deterministic semantics, Automated theorem proving by resolution in non-classical logics, Proof theory for locally finite many-valued logics: semi-projective logics, Higher-level inferences in the strong-Kleene setting: a proof-theoretic approach, A first polynomial non-clausal class in many-valued logic, Axiomatizing non-deterministic many-valued generalized consequence relations, Bisequent calculus for four-valued quasi-relevant logics: cut elimination and interpolation, Proof search and co-NP completeness for many-valued logics, Fibrational Semantics for Many-Valued Logic Programs: Grounds for Non-Groundness, Partial and paraconsistent three-valued logics, Complexity of clausal constraints over chains, Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\), Non-distributive relatives of ETL and NFL, Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis, Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics, Classic-Like Analytic Tableaux for Finite-Valued Logics, On the refutational completeness of signed binary resolution and hyperresolution, From bi-facial truth to bi-facial proofs