A fixpoint semantics of Horn sentences based on substitution sets

DOI10.1016/0304-3975(87)90039-9zbMath0641.68147OpenAlexW1991749458MaRDI QIDQ1100934

Shuji Doshita, Mikio Yoshida, Susumu Yamasaki

Publication date: 1987

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

Full work available at URL: https://doi.org/10.1016/0304-3975(87)90039-9

zbMATH Keywords

Horn clausesdenotational semanticslogic programmingunit deductionunsatisfiable Horn sentences

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

A New Algorithm for Computing Least Generalization of a Set of Atoms, Declarative modeling of the operational behavior of logic languages, Recursion equation sets computing logic programs, A compositional semantics for logic programs

Cites Work

• Unnamed Item
• Unnamed Item
• A new combination of input and unit deductions for Horn sentences
• Contributions to the Theory of Logic Programming
• Unit Refutations and Horn Sets
• The Semantics of Predicate Logic as a Programming Language
• Another Generalization of Resolution
• Resolution With Merging
• The Specialization of Programs by Theorem Proving