scientific article; zbMATH DE number 3344563

MaRDI QIDQ5620583zbMATH OpenFDO

Authors Stig Kanger

Publication date 1963

zbMATH Keywords

computer sciencemathematical logic

Mathematics Subject Classification ID

Classical first-order logic (03B10) Proof theory in general (including proof-theoretic semantics) (03F03)

Cited in

(13)

• Modal translations in substructural logics
• Cut-type rules for calculi of general type
• Evidence algorithm and SAD systems: past and possible future
• Sequent forms of Herbrand theorem and their applications
• Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
• Evidence algorithm and inference search in first-order logics
• What is essential unification?
• Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification
• Glushkov's evidence algorithm
• The elimination of atomic cuts and the semishortening property for Gentzen's sequent calculus with equality
• What you always wanted to know about rigid \(E\)-unification
• The undecidability of simultaneous rigid E-unification
• Superposition-based equality handling for analytic tableaux

This page was built for publication:

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