Proving infinitary formulas

DOI10.1017/S1471068416000302MaRDI QIDQ4593059zbMATH OpenFDO

Authors Amelia Harrison, Vladimir Lifschitz, Julian Michael

Publication date 9 November 2017

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1608.01626

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17)

Abstract: The infinitary propositional logic of here-and-there is important for the theory of answer set programming in view of its relation to strongly equivalent transformations of logic programs. We know a formal system axiomatizing this logic exists, but a proof in that system may include infinitely many formulas. In this note we describe a relationship between the validity of infinitary formulas in the logic of here-and-there and the provability of formulas in some finite deductive systems. This relationship allows us to use finite proofs to justify the validity of infinitary formulas. This note is under consideration for publication in Theory and Practice of Logic Programming.

Recommendations

• Proving infinite satisfiability
• Proving Infinitary Normalization
• Infinitary affine proofs
• A reduction-principle for infinite formulas
• scientific article; zbMATH DE number 1431685
• scientific article; zbMATH DE number 1136111
• Proof systems for infinite behaviours
• scientific article; zbMATH DE number 3919854
• Infinitary proof theory: the multiplicative additive case

Cites work

• A Characterization of Strong Equivalence for Logic Programs with Variables
• A short introduction to intuitionistic logic
• Abstract gringo
• Correct reasoning. Essays on logic-based AI in honour of Vladimir Lifschitz
• Handbook of knowledge representation.
• scientific article; zbMATH DE number 3250542 (Why is no real title available?)
• Infinitary Equilibrium Logic and Strong Equivalence
• On equivalence of infinitary formulas under the stable model semantics
• On intermediate many-valued logics

Cited in

(4)

• Infinitary equilibrium logic and strongly equivalent logic programs
• scientific article; zbMATH DE number 3939323 (Why is no real title available?)
• On evaluations of propositional formulas in countable structures
• Proof of the law of infinite conjunction using the perfect disjunctive normal form

Describes a project that uses

Uses Software

• Gringo

This page was built for publication: Proving infinitary formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4593059)