The Blossom of Finite Semantic Trees

DOI10.1007/978-3-642-37651-1_5zbMath1383.03017OpenAlexW199417883MaRDI QIDQ4916075

Jean-Pierre Jouannaud, Jean Goubault-Larrecq

Publication date: 19 April 2013

Published in: Programming Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-37651-1_5

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (2)

Formalization of the resolution calculus for first-order logic ⋮ Set of support, demodulation, paramodulation: a historical perspective

Uses Software

• SPASS

Cites Work

• Deciding \(\mathcal H_1\) by resolution
• Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically
• Resolution Strategies as Decision Procedures
• Equational inference, canonical proofs, and proof orderings
• Proving refutational completeness of theorem-proving strategies
• Logic for Programming, Artificial Intelligence, and Reasoning
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The Blossom of Finite Semantic Trees