Unsorted Functional Translations

DOI10.1016/j.entcs.2011.10.002zbMath1347.03037OpenAlexW1976699340WikidataQ113318207 ScholiaQ113318207MaRDI QIDQ2825403

Carlos Areces, Daniel Gorín

Publication date: 7 October 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2011.10.002

zbMATH Keywords

sortsautomated theorem provingfunctional translation

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35)

Related Items

A prover dealing with nominals, binders, transitivity and relation hierarchies

Uses Software

• SPASS

Cites Work

• Decidability by resolution for propositional modal logics
• System Description: Spass Version 3.0
• Modal Theorem Proving: An Equational Viewpoint
• Resolution Strategies as Decision Procedures
• Functional translation and second-order frame properties of modal logics
• An empirical analysis of modal theorem provers
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item