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

DOI10.1007/3-540-61208-4_16MaRDI QIDQ4645241zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 3649012 (Why is no real title available?)
• scientific article; zbMATH DE number 4055570 (Why is no real title available?)
• scientific article; zbMATH DE number 4080961 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 3577484 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• An Efficient Unification Algorithm
• Automated reasoning contributes to mathematics and logic
• On Matrices with Connections
• SETHEO: A high-performance theorem prover
• The foundations of mathematics. A study in the philosophy of science
• \textsf{Ko\(_{\mathsf{M}}\)eT}

Cited in

(10)

• Intuitionistic Letcc via Labelled Deduction
• Representing scope in intuitionistic deductions
• \(\mathsf{ileanTAP}\): an intuitionistic theorem prover
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
• A tableau method for the Lambek calculus based on a matrix characterization
• 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

Describes a project that uses

Uses Software

• KoMeT
• SETHEO

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)