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

DOI10.1007/3-540-61208-4_16zbMath1412.68251OpenAlexW2134977256MaRDI QIDQ4645241

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

Related Items (10)

IeanCOP: lean connection-based theorem proving ⋮ ileanTAP: An intuitionistic theorem prover ⋮ leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) ⋮ Converting non-classical matrix proofs into sequent-style systems ⋮ A Tableau Method for the Lambek Calculus based on a Matrix Characterization ⋮ Representing scope in intuitionistic deductions ⋮ Intuitionistic Letcc via Labelled Deduction ⋮ Connection-based proof construction in linear logic ⋮ A Proof-Planning Framework with explicit Abstractions based on Indexed Formulas ⋮ A connection-based characterization of bi-intuitionistic validity

Uses Software

• SETHEO
• KoMeT

Cites Work

• The foundations of mathematics. A study in the philosophy of science
• SETHEO: A high-performance theorem prover
• On Matrices with Connections
• An Efficient Unification Algorithm
• KoMeT
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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