Connection calculus theorem proving with multiple built-in theories

DOI10.1006/jsco.1999.0365zbMath0967.68150OpenAlexW2127942206MaRDI QIDQ5927987

Uwe Petermann

Publication date: 19 March 2001

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jsco.1999.0365

zbMATH Keywords

automated reasoningdeduction systems

Mathematics Subject Classification ID

Related Items (2)

Sharp asymptotics for the partition function of some continuous-time directed polymers ⋮ Superdiffusivity for a Brownian polymer in a continuous Gaussian environment

Uses Software

• ProCom
• CaPrI

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
• Multimodal logic programming using equational and order-sorted logic
• A resolution principle for constrained logics
• Automated deduction by theory resolution
• Theorem proving with analytic tableaux and related methods. 4th international workshop, TABLEAUX '95, Schloß Rheinfels, St. Goar, Germany, May 7-10, 1995. Proceedings
• Functional translation and second-order frame properties of modal logics
• A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi

This page was built for publication: Connection calculus theorem proving with multiple built-in theories