Cyclic connections

DOI10.1007/3-540-61208-4_6zbMath1415.03017OpenAlexW2912823222MaRDI QIDQ4645228

Gérard Becher

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_6

zbMATH Keywords

query languagetree automatonbackground theoryopen formulapredicate symbol

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Cites Work

• The undecidability of simultaneous rigid E-unification
• Completeness of a prover for dense linear orders
• Automated deduction by theory resolution
• Ordered chaining calculi for first-order theories of transitive relations
• Fast Decision Procedures Based on Congruence Closure
• Theorem Proving via General Matings
• Theorem proving using equational matings and rigid E -unification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item