scientific article

Publication date: 23 January 1993

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

modal logic proof theory semantics intuitionistic logic classical logic automated deduction first-order logics matrix characterisation classical sequent calculi modal sequent calculi

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

A tableau-like proof procedure for normal modal logics ⋮ Evidence algorithm and inference search in first-order logics ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ On proof normalization in linear logic ⋮ A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics ⋮ The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Crystal: Integrating structured queries into a tactic language ⋮ Indexed systems of sequents and cut-elimination ⋮ Increasing the efficiency of automated theorem proving ⋮ Unification theory ⋮ Liberalized variable splitting ⋮ A proof-search procedure for intuitionistic propositional logic ⋮ TPS: A theorem-proving system for classical type theory ⋮ Multimodal linguistic inference ⋮ Direct deductive computation on discourse representation structures ⋮ Some general results about proof normalization ⋮ Contraction-free sequent calculi for intuitionistic logic ⋮ Herbrand's fundamental theorem in the eyes of Jean van Heijenoort ⋮ Incremental variable splitting ⋮ \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps ⋮ Hintikka multiplicities in matrix decision methods for some propositional modal logics ⋮ ileanTAP: An intuitionistic theorem prover ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ Proof analysis in intermediate logics ⋮ Labelling ideality and subideality ⋮ Hilbert's epsilon as an operator of indefinite committed choice ⋮ Proof-terms for classical and intuitionistic resolution ⋮ Distributed modal theorem proving with KE ⋮ T-string unification: Unifying prefixes in non-classical proof methods ⋮ On the intuitionistic force of classical search (Extended abstract) ⋮ Proof-search in intuitionistic logic based on constraint satisfaction ⋮ A resolution theorem prover for intuitionistic logic ⋮ Converting non-classical matrix proofs into sequent-style systems ⋮ On negation: Pure local rules ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ Representing scope in intuitionistic deductions ⋮ Intuitionistic Letcc via Labelled Deduction ⋮ A first step towardsmodeling semistructured data in hybrid multimodal logic ⋮ Deciding intuitionistic propositional logic via translation into classical logic ⋮ Connection-based proof construction in linear logic ⋮ Temporal reasoning over linear discrete time ⋮ A Proof-Planning Framework with explicit Abstractions based on Indexed Formulas ⋮ A Category-Theoretic Approach to Social Network Analysis ⋮ Simplification of boolean verification conditions ⋮ On the intuitionistic force of classical search ⋮ Connection methods in linear logic and proof nets construction ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Structural cut elimination. I: Intuitionistic and classical logic ⋮ A uniform procedure for converting matrix proofs into sequent-style systems ⋮ From Schütte’s Formal Systems to Modern Automated Deduction ⋮ A proof procedure for the logic of hereditary Harrop formulas ⋮ Testing XML constraint satisfiability ⋮ Hypothesis finding with proof theoretical appropriateness criteria