T-string unification: unifying prefixes in non-classical proof methods

DOI10.1007/3-540-61208-4_16zbMATH Open1412.68251OpenAlexW2134977256MaRDI QIDQ4645241FDOQ4645241

Authors: Jens Otten, Christoph Kreitz 

Publication date: 10 January 2019

Published in: Theorem Proving with Analytic Tableaux and Related Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61208-4_16

Recommendations

• scientific article; zbMATH DE number 1189062
• Non-clausal connection calculi for non-classical logics
• scientific article; zbMATH DE number 1543301
• Remarks about the unification type of several non-symmetric non-transitive modal logics
• UNIFICATION IN INTERMEDIATE LOGICS

zbMATH Keywords

modal logicaccessibility relationtransformation ruleatomic formulageneral unifier

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• An Efficient Unification Algorithm
• A Machine-Oriented Logic Based on the Resolution Principle
• SETHEO: A high-performance theorem prover
• Title not available (Why is that?)
• The foundations of mathematics. A study in the philosophy of science
• Title not available (Why is that?)
• Title not available (Why is that?)
• On Matrices with Connections
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated reasoning contributes to mathematics and logic
• Title not available (Why is that?)
• \textsf{Ko\(_{\mathsf{M}}\)eT}

Cited In (10)

• Intuitionistic Letcc via Labelled Deduction
• Representing scope in intuitionistic deductions
• \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
• A tableau method for the Lambek calculus based on a matrix characterization
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• A connection-based characterization of bi-intuitionistic validity
• A proof-planning framework with explicit abstractions based on indexed formulas
• IeanCOP: lean connection-based theorem proving
• Connection-based proof construction in linear logic
• Converting non-classical matrix proofs into sequent-style systems

Uses Software

• SETHEO
• KoMeT

This page was built for publication: T-string unification: unifying prefixes in non-classical proof methods

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