A proof system for the first-order relational calculus

DOI10.1016/0022-0000(80)90007-0zbMath0431.68084OpenAlexW2027612506MaRDI QIDQ1138391

Matthew C. B. Hennessy

Publication date: 1980

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(80)90007-0

zbMATH Keywords

proof systemcompactness theoremanalytic tableaux methodfirst-order relational calculus

Mathematics Subject Classification ID

Algebraic logic (03G99)

Related Items

Peirce algebras, Dynamic logic with program specifications and its relational proof system, Complexity of equations valid in algebras of relations. I: Strong non-finitizability, Floyd's principle, correctness theories and program equivalence, Algebraization of quantifier logics, an introductory overview, A Completeness Result for Relation Algebra with Binders, An efficient relational deductive system for propositional non-classical logics, A sequent calculus for relation algebras

Cites Work

• The representation of relational algebras
• The Semantics of Call-By-Value and Call-By-Name in a Nondeterministic Environment
• On the termination of program schemas
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item