Showing 1–17 of 17 results for author: Marek, V

The Evolution of Rough Sets 1970s-1981

Authors: Viktor Marek, Ewa Orłowska, Ivo Düntsch

Abstract: In this note research and publications by Zdzisław Pawlak and his collaborators from 1970s and 1981 are recalled. Focus is placed on the sources of inspiration which one can identify on the basis of those publications. Finally, developments from 1981 related to rough sets and information systems are outlined. In this note research and publications by Zdzisław Pawlak and his collaborators from 1970s and 1981 are recalled. Focus is placed on the sources of inspiration which one can identify on the basis of those publications. Finally, developments from 1981 related to rough sets and information systems are outlined. △ Less

Submitted 8 April, 2025; originally announced May 2025.

Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer

Authors: Marijn J. H. Heule, Oliver Kullmann, Victor W. Marek

Abstract: The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set N = $\{1, 2, ...\}$ of natural numbers be divided into two parts, such that no part contains a triple $(a,b,c)$ with $a^2 + b^2 = c^2$ ? A prize for the solution was offered by Ronald Graham over two decades ago. We solve this problem, proving in fact the impossibility, by using the Cube-an… ▽ More The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set N = $\{1, 2, ...\}$ of natural numbers be divided into two parts, such that no part contains a triple $(a,b,c)$ with $a^2 + b^2 = c^2$ ? A prize for the solution was offered by Ronald Graham over two decades ago. We solve this problem, proving in fact the impossibility, by using the Cube-and-Conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking. △ Less

Submitted 2 May, 2016; originally announced May 2016.

Journal ref: SAT 2016, LNCS 9710, pages 228-245

Index sets for Finite Normal Predicate Logic Programs

Authors: D. Cenzer, V. W. Marek, J. B. Remmel

Abstract: <Q>_e is the effective list of all finite predicate logic programs. <T_e> is the list of recursive trees. We modify constructions of Marek, Nerode, and Remmel [25] to construct recursive functions f and g such that for all indices e, (i) there is a one-to-one degree preserving correspondence between the set of stable models of Q_e and the set of infinite paths through T_{f(e)} and (ii) there is a… ▽ More <Q>_e is the effective list of all finite predicate logic programs. <T_e> is the list of recursive trees. We modify constructions of Marek, Nerode, and Remmel [25] to construct recursive functions f and g such that for all indices e, (i) there is a one-to-one degree preserving correspondence between the set of stable models of Q_e and the set of infinite paths through T_{f(e)} and (ii) there is a one-to-one degree preserving correspondence between the set of infinite paths through T_e and the set of stable models of Q_{g(e)}. We use these two recursive functions to reduce the problem of finding the complexity of the index set I_P for various properties P of normal finite predicate logic programs to the problem of computing index sets for primitive recursive trees for which there is a large variety of results [6], [8], [16], [17], [18], [19]. We use our correspondences to determine the complexity of the index sets of all programs and of certain special classes of finite predicate logic programs of properties such as (i) having no stable models, (ii) having at least one stable model, (iii) having exactly c stable models for any given positive integer c, (iv) having only finitely many stable models, or (vi) having infinitely many stable models. △ Less

Submitted 26 March, 2013; originally announced March 2013.

Comments: 55 pages

ACM Class: F.1.3; F.4.1

Origins of Answer-Set Programming - Some Background And Two Personal Accounts

Authors: Victor W. Marek, Ilkka Niemela, Miroslaw Truszczynski

Abstract: We discuss the evolution of aspects of nonmonotonic reasoning towards the computational paradigm of answer-set programming (ASP). We give a general overview of the roots of ASP and follow up with the personal perspective on research developments that helped verbalize the main principles of ASP and differentiated it from the classical logic programming. We discuss the evolution of aspects of nonmonotonic reasoning towards the computational paradigm of answer-set programming (ASP). We give a general overview of the roots of ASP and follow up with the personal perspective on research developments that helped verbalize the main principles of ASP and differentiated it from the classical logic programming. △ Less

Submitted 16 August, 2011; originally announced August 2011.

Comments: In G. Brewka, V.M. Marek, and M. Truszczynski, eds. Nonmonotonic Reasoning -- Essays Celebrating its 30th Anniversary, College Publications, 2011 (a volume of papers presented at NonMon at 30 meeting, Lexington, KY, USA, October 2010)

MSC Class: I.2.4

Reiter's Default Logic Is a Logic of Autoepistemic Reasoning And a Good One, Too

Authors: Marc Denecker, Victor W. Marek, Miroslaw Truszczynski

Abstract: A fact apparently not observed earlier in the literature of nonmonotonic reasoning is that Reiter, in his default logic paper, did not directly formalize informal defaults. Instead, he translated a default into a certain natural language proposition and provided a formalization of the latter. A few years later, Moore noted that propositions like the one used by Reiter are fundamentally different t… ▽ More A fact apparently not observed earlier in the literature of nonmonotonic reasoning is that Reiter, in his default logic paper, did not directly formalize informal defaults. Instead, he translated a default into a certain natural language proposition and provided a formalization of the latter. A few years later, Moore noted that propositions like the one used by Reiter are fundamentally different than defaults and exhibit a certain autoepistemic nature. Thus, Reiter had developed his default logic as a formalization of autoepistemic propositions rather than of defaults. The first goal of this paper is to show that some problems of Reiter's default logic as a formal way to reason about informal defaults are directly attributable to the autoepistemic nature of default logic and to the mismatch between informal defaults and the Reiter's formal defaults, the latter being a formal expression of the autoepistemic propositions Reiter used as a representation of informal defaults. The second goal of our paper is to compare the work of Reiter and Moore. While each of them attempted to formalize autoepistemic propositions, the modes of reasoning in their respective logics were different. We revisit Moore's and Reiter's intuitions and present them from the perspective of autotheoremhood, where theories can include propositions referring to the theory's own theorems. We then discuss the formalization of this perspective in the logics of Moore and Reiter, respectively, using the unifying semantic framework for default and autoepistemic logics that we developed earlier. We argue that Reiter's default logic is a better formalization of Moore's intuitions about autoepistemic propositions than Moore's own autoepistemic logic. △ Less

Submitted 16 August, 2011; originally announced August 2011.

Comments: In G. Brewka, V.M. Marek, and M. Truszczynski, eds. Nonmonotonic Reasoning -- Essays Celebrating its 30th Anniversary, College Publications, 2011 (a volume of papers presented at NonMOn at 30 meeting, Lexington, KY, USA, October 2010

MSC Class: I.2.4

An Application of Proof-Theory in Answer Set Programming

Authors: V. W. Marek, J. B. Remmel

Abstract: We apply proof-theoretic techniques in answer Set Programming. The main results include: 1. A characterization of continuity properties of Gelfond-Lifschitz operator for logic program. 2. A propositional characterization of stable models of logic programs (without referring to loop formulas. We apply proof-theoretic techniques in answer Set Programming. The main results include: 1. A characterization of continuity properties of Gelfond-Lifschitz operator for logic program. 2. A propositional characterization of stable models of logic programs (without referring to loop formulas. △ Less

Submitted 11 January, 2010; v1 submitted 2 May, 2009; originally announced May 2009.

Comments: 22 pages. Short version was published in ICLP08. New version slightly shorter than the previous version

Guarded resolution for answer set programming

Authors: V. W. Marek, J. B. Remmel

Abstract: We describe a variant of resolution rule of proof and show that it is complete for stable semantics of logic programs. We show applications of this result. We describe a variant of resolution rule of proof and show that it is complete for stable semantics of logic programs. We show applications of this result. △ Less

Submitted 21 February, 2010; v1 submitted 24 April, 2009; originally announced April 2009.

Comments: 13 pages, some results added. Accepted for publication at TPLP

Logic programs with monotone abstract constraint atoms

Authors: V. W. Marek, I. Niemela, M. Truszczynski]

Abstract: We introduce and study logic programs whose clauses are built out of monotone constraint atoms. We show that the operational concept of the one-step provability operator generalizes to programs with monotone constraint atoms, but the generalization involves nondeterminism. Our main results demonstrate that our formalism is a common generalization of (1) normal logic programming with its semantic… ▽ More We introduce and study logic programs whose clauses are built out of monotone constraint atoms. We show that the operational concept of the one-step provability operator generalizes to programs with monotone constraint atoms, but the generalization involves nondeterminism. Our main results demonstrate that our formalism is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with weight atoms (lparse programs) with the semantics of stable models, as defined by Niemela, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue. △ Less

Submitted 25 August, 2006; originally announced August 2006.

Comments: 33 pages

ACM Class: F.4.1; D.1.6

On the Expressibility of Stable Logic Programming

Authors: Victor W. Marek, Jeffrey B. Remmel

Abstract: (We apologize for pidgin LaTeX) Schlipf \cite{sch91} proved that Stable Logic Programming (SLP) solves all $\mathit{NP}$ decision problems. We extend Schlipf's result to prove that SLP solves all search problems in the class $\mathit{NP}$. Moreover, we do this in a uniform way as defined in \cite{mt99}. Specifically, we show that there is a single $\mathrm{DATALOG}^{\neg}$ program… ▽ More (We apologize for pidgin LaTeX) Schlipf \cite{sch91} proved that Stable Logic Programming (SLP) solves all $\mathit{NP}$ decision problems. We extend Schlipf's result to prove that SLP solves all search problems in the class $\mathit{NP}$. Moreover, we do this in a uniform way as defined in \cite{mt99}. Specifically, we show that there is a single $\mathrm{DATALOG}^{\neg}$ program $P_{\mathit{Trg}}$ such that given any Turing machine $M$, any polynomial $p$ with non-negative integer coefficients and any input $σ$ of size $n$ over a fixed alphabet $Σ$, there is an extensional database $\mathit{edb}_{M,p,σ}$ such that there is a one-to-one correspondence between the stable models of $\mathit{edb}_{M,p,σ} \cup P_{\mathit{Trg}}$ and the accepting computations of the machine $M$ that reach the final state in at most $p(n)$ steps. Moreover, $\mathit{edb}_{M,p,σ}$ can be computed in polynomial time from $p$, $σ$ and the description of $M$ and the decoding of such accepting computations from its corresponding stable model of $\mathit{edb}_{M,p,σ} \cup P_{\mathit{Trg}}$ can be computed in linear time. A similar statement holds for Default Logic with respect to $Σ_2^\mathrm{P}$-search problems\footnote{The proof of this result involves additional technical complications and will be a subject of another publication.}. △ Less

Submitted 22 December, 2003; originally announced December 2003.

Comments: 17 pages

ACM Class: F.4.1

Journal ref: TCLP 3(2003), pp. 551-567q

Satisfiability and computing van der Waerden numbers

Authors: Michael R. Dransfield, Victor W. Marek, Miroslaw Truszczynski

Abstract: In this paper we bring together the areas of combinatorics and propositional satisfiability. Many combinatorial theorems establish, often constructively, the existence of positive integer functions, without actually providing their closed algebraic form or tight lower and upper bounds. The area of Ramsey theory is especially rich in such results. Using the problem of computing van der Waerden nu… ▽ More In this paper we bring together the areas of combinatorics and propositional satisfiability. Many combinatorial theorems establish, often constructively, the existence of positive integer functions, without actually providing their closed algebraic form or tight lower and upper bounds. The area of Ramsey theory is especially rich in such results. Using the problem of computing van der Waerden numbers as an example, we show that these problems can be represented by parameterized propositional theories in such a way that decisions concerning their satisfiability determine the numbers (function) in question. We show that by using general-purpose complete and local-search techniques for testing propositional satisfiability, this approach becomes effective -- competitive with specialized approaches. By following it, we were able to obtain several new results pertaining to the problem of computing van der Waerden numbers. We also note that due to their properties, especially their structural simplicity and computational hardness, propositional theories that arise in this research can be of use in development, testing and benchmarking of SAT solvers. △ Less

Submitted 31 October, 2003; originally announced October 2003.

Comments: Proceedings of SAT-2003, LNCS, Springer Verlag

ACM Class: I.2.8; F.4.1

Logic programs with monotone cardinality atoms

Authors: Victor W. Marek, Ilkka Niemela, Miroslaw Truszczynski

Abstract: We investigate mca-programs, that is, logic programs with clauses built of monotone cardinality atoms of the form kX, where k is a non-negative integer and X is a finite set of propositional atoms. We develop a theory of mca-programs. We demonstrate that the operational concept of the one-step provability operator generalizes to mca-programs, but the generalization involves nondeterminism. Our m… ▽ More We investigate mca-programs, that is, logic programs with clauses built of monotone cardinality atoms of the form kX, where k is a non-negative integer and X is a finite set of propositional atoms. We develop a theory of mca-programs. We demonstrate that the operational concept of the one-step provability operator generalizes to mca-programs, but the generalization involves nondeterminism. Our main results show that the formalism of mca-programs is a common generalization of (1) normal logic programming with its semantics of models, supported models and stable models, (2) logic programming with cardinality atoms and with the semantics of stable models, as defined by Niemela, Simons and Soininen, and (3) of disjunctive logic programming with the possible-model semantics of Sakama and Inoue. △ Less

Submitted 31 October, 2003; originally announced October 2003.

Comments: Proceedings of LPNMR-03 (7th International Conference), LNCS, Springer Verlag

ACM Class: D.1.6; I.2.3

Ultimate approximations in nonmonotonic knowledge representation systems

Authors: Marc Denecker, Victor W. Marek, Miroslaw Truszczynski

Abstract: We study fixpoints of operators on lattices. To this end we introduce the notion of an approximation of an operator. We order approximations by means of a precision ordering. We show that each lattice operator O has a unique most precise or ultimate approximation. We demonstrate that fixpoints of this ultimate approximation provide useful insights into fixpoints of the operator O. We apply our… ▽ More We study fixpoints of operators on lattices. To this end we introduce the notion of an approximation of an operator. We order approximations by means of a precision ordering. We show that each lattice operator O has a unique most precise or ultimate approximation. We demonstrate that fixpoints of this ultimate approximation provide useful insights into fixpoints of the operator O. We apply our theory to logic programming and introduce the ultimate Kripke-Kleene, well-founded and stable semantics. We show that the ultimate Kripke-Kleene and well-founded semantics are more precise then their standard counterparts We argue that ultimate semantics for logic programming have attractive epistemological properties and that, while in general they are computationally more complex than the standard semantics, for many classes of theories, their complexity is no worse. △ Less

Submitted 11 May, 2002; originally announced May 2002.

Comments: This paper was published in Principles of Knowledge Representation and Reasoning, Proceedings of the Eighth International Conference (KR2002)

ACM Class: I.2.4

Annotated revision programs

Authors: Victor Marek, Inna Pivkina, Miroslaw Truszczynski

Abstract: Revision programming is a formalism to describe and enforce updates of belief sets and databases. That formalism was extended by Fitting who assigned annotations to revision atoms. Annotations provide a way to quantify the confidence (probability) that a revision atom holds. The main goal of our paper is to reexamine the work of Fitting, argue that his semantics does not always provide results c… ▽ More Revision programming is a formalism to describe and enforce updates of belief sets and databases. That formalism was extended by Fitting who assigned annotations to revision atoms. Annotations provide a way to quantify the confidence (probability) that a revision atom holds. The main goal of our paper is to reexamine the work of Fitting, argue that his semantics does not always provide results consistent with intuition, and to propose an alternative treatment of annotated revision programs. Our approach differs from that proposed by Fitting in two key aspects: we change the notion of a model of a program and we change the notion of a justified revision. We show that under this new approach fundamental properties of justified revisions of standard revision programs extend to the annotated case. △ Less

Submitted 19 July, 2001; originally announced July 2001.

Comments: 30 pages, to appear in Artificial Intelligence Journal

ACM Class: I.2.4; I.2.3

Journal ref: Artificial Intelligence Journal, 138 (2002), pp. 149-180.

Uniform semantic treatment of default and autoepistemic logics

Authors: Marc Denecker, Victor W. Marek, Miroslaw Truszczynski

Abstract: We revisit the issue of connections between two leading formalisms in nonmonotonic reasoning: autoepistemic logic and default logic. For each logic we develop a comprehensive semantic framework based on the notion of a belief pair. The set of all belief pairs together with the so called knowledge ordering forms a complete lattice. For each logic, we introduce several semantics by means of fixpoi… ▽ More We revisit the issue of connections between two leading formalisms in nonmonotonic reasoning: autoepistemic logic and default logic. For each logic we develop a comprehensive semantic framework based on the notion of a belief pair. The set of all belief pairs together with the so called knowledge ordering forms a complete lattice. For each logic, we introduce several semantics by means of fixpoints of operators on the lattice of belief pairs. Our results elucidate an underlying isomorphism of the respective semantic constructions. In particular, we show that the interpretation of defaults as modal formulas proposed by Konolige allows us to represent all semantics for default logic in terms of the corresponding semantics for autoepistemic logic. Thus, our results conclusively establish that default logic can indeed be viewed as a fragment of autoepistemic logic. However, as we also demonstrate, the semantics of Moore and Reiter are given by different operators and occupy different locations in their corresponding families of semantics. This result explains the source of the longstanding difficulty to formally relate these two semantics. In the paper, we also discuss approximating skeptical reasoning with autoepistemic and default logics and establish constructive principles behind such approximations. △ Less

Submitted 3 February, 2000; originally announced February 2000.

Comments: Proceedings of the Seventh International Conference on Principles of Knowledge Representation and Reasoning (KR2000); 11 pages

ACM Class: I.2.3; I.2.4

Journal ref: Artificial Intelligence Journal, 143 (2003), pp. 79--122

Representation Theory for Default Logic

Authors: Victor Marek, Jan Treur, Miroslaw Truszczynski

Abstract: Default logic can be regarded as a mechanism to represent families of belief sets of a reasoning agent. As such, it is inherently second-order. In this paper, we study the problem of representability of a family of theories as the set of extensions of a default theory. We give a complete solution to the representability by means of normal default theories. We obtain partial results on representa… ▽ More Default logic can be regarded as a mechanism to represent families of belief sets of a reasoning agent. As such, it is inherently second-order. In this paper, we study the problem of representability of a family of theories as the set of extensions of a default theory. We give a complete solution to the representability by means of normal default theories. We obtain partial results on representability by arbitrary default theories. We construct examples of denumerable families of non-including theories that are not representable. We also study the concept of equivalence between default theories. △ Less

Submitted 28 January, 1999; originally announced January 1999.

Comments: Annals of Mathematics and Artificial Intelligence, 21 (1997), pp. 343-358

ACM Class: I.2.4, F.4.1, I.2.3

Fixpoint 3-valued semantics for autoepistemic logic

Authors: M. Denecker, V. Marek, M. Truszczynski

Abstract: The paper presents a constructive fixpoint semantics for autoepistemic logic (AEL). This fixpoint characterizes a unique but possibly three-valued belief set of an autoepistemic theory. It may be three-valued in the sense that for a subclass of formulas F, the fixpoint may not specify whether F is believed or not. The paper presents a constructive 3-valued semantics for autoepistemic logic (AEL)… ▽ More The paper presents a constructive fixpoint semantics for autoepistemic logic (AEL). This fixpoint characterizes a unique but possibly three-valued belief set of an autoepistemic theory. It may be three-valued in the sense that for a subclass of formulas F, the fixpoint may not specify whether F is believed or not. The paper presents a constructive 3-valued semantics for autoepistemic logic (AEL). We introduce a derivation operator and define the semantics as its least fixpoint. The semantics is 3-valued in the sense that, for some formulas, the least fixpoint does not specify whether they are believed or not. We show that complete fixpoints of the derivation operator correspond to Moore's stable expansions. In the case of modal representations of logic programs our least fixpoint semantics expresses well-founded semantics or 3-valued Fitting-Kunen semantics (depending on the embedding used). We show that, computationally, our semantics is simpler than the semantics proposed by Moore (assuming that the polynomial hierarchy does not collapse). △ Less

Submitted 12 January, 1999; originally announced January 1999.

Comments: Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI-98), pages 840--845, (MIT Press, 1998)

ACM Class: I.2.4, F.4.1, I.2.3

Stable models and an alternative logic programming paradigm

Authors: Victor W. Marek, Miroslaw Truszczynski

Abstract: In this paper we reexamine the place and role of stable model semantics in logic programming and contrast it with a least Herbrand model approach to Horn programs. We demonstrate that inherent features of stable model semantics naturally lead to a logic programming system that offers an interesting alternative to more traditional logic programming styles of Horn logic programming, stratified log… ▽ More In this paper we reexamine the place and role of stable model semantics in logic programming and contrast it with a least Herbrand model approach to Horn programs. We demonstrate that inherent features of stable model semantics naturally lead to a logic programming system that offers an interesting alternative to more traditional logic programming styles of Horn logic programming, stratified logic programming and logic programming with well-founded semantics. The proposed approach is based on the interpretation of program clauses as constraints. In this setting programs do not describe a single intended model, but a family of stable models. These stable models encode solutions to the constraint satisfaction problem described by the program. Our approach imposes restrictions on the syntax of logic programs. In particular, function symbols are eliminated from the language. We argue that the resulting logic programming system is well-attuned to problems in the class NP, has a well-defined domain of applications, and an emerging methodology of programming. We point out that what makes the whole approach viable is recent progress in implementations of algorithms to compute stable models of propositional logic programs. △ Less

Submitted 18 September, 1998; originally announced September 1998.

Comments: 21 pages

ACM Class: I.2.3, I.2.4

Journal ref: The Logic Programming Paradigm, K.R. Apt, V.W. Marek, M. Truszczynski, D.S. Warren (eds.), pp. 375-398. Springer-Verlag, 1999