Handling transitive relations in first-order automated reasoning

DOI10.1007/s10817-021-09605-zOpenAlexW3201112613MaRDI QIDQ2069868

Koen Claessen, Ann Lillieström

Publication date: 21 January 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-021-09605-z

zbMATH Keywords

first-order logicautomated reasoningtransformationtransitivityautomated theorem provingbinary relationstransitive relations

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• VAMPIRE
• SPASS
• TPTP
• z3
• Kodkod
• CVC4

Cites Work

• Relational constraint solving in SMT
• Ordered chaining calculi for first-order theories of transitive relations
• A Decision Procedure for Sets, Binary Relations and Partial Functions
• From Search to Computation: Redundancy Criteria and Simplification at Work
• The TPTP problem library
• The axiomatic translation principle for modal logic
• Kodkod: A Relational Model Finder

This page was built for publication: Handling transitive relations in first-order automated reasoning