The classical algebraic modelling approach for integer programming (IP) is not suitable for some real world IP problems, since the algebraic formulations allow only for the description of mathematical relations, not logical relations. In this paper, we present a language + for IP, in which we write logical specification of an IP problem. + is a language based on the predicate logic, but is extended with meta predicates such as at_least(m,S), where m is a non-negative integer, meaning that at least m predicates in the set S of formulas hold. The meta predicates facilitate reasoning about a model of an IP problem rigorously and logically. + is executable in the sense that formulas in + are mechanically translated into a set of mathematical formulas, called IP formulas, which most of existing IP solvers accept. We give a systematic method for translating formulas in + to IP formulas. The translation is rigorously defined, verified and implemented in Mathematica 3.0. Our work follows the approach of McKinnon and Williams, and elaborated the language in that (1) it is rigorously defined, (2) transformation to IP formulas is more optimised and verified, and (3) the transformation is completely given in Mathematica 3.0 and is integrated into IP solving environment as a tool for IP.

The subject of the paper is to analyze time complexity of the minimum modification problem in the Horn clause propositional logic. Given a set H of Horn clauses and a query Q in propositional logic, we say that Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens among clauses of H. Suppose that Q is not provable over H, and we are going to modify H and Q into H and Q , respectively, such that Q is provable over H . The problem of making such modification by minimum variable deletion (MVD), by minimum clause addition (MCA) or by their combination (MVDCA) is considered. Each problem is shown to be NP-complete, and some approximation algorithms with their experimental evaluation are given.

The subject of the paper is to analyze time complexity of the minimum axiom set problem (MASHC) in the Horn clause propositional logic. MASHC is defined by "Given a set H of Horn clauses and a query Q, all in propositional logic, such that Q is provable over H, find an axiom set of minimum cardinality, HH, with respect to Q, where Q is provable over H if and only if Q can be shown to be true by repeating Modus Ponens starting from clauses of H under the assumption that all of them are originally assumed to be true". If Q is provable over H then H is called an axiom set (with respect to Q). As stated in the definition of MASHC, detecting if Q is provable over H is required. This leads us to a problem, called the provability detecting problem (PDPHC), defined by "Given a set H of Horn clauses and a query Q in propositional logic, determine if Q is provable over H". First an O(σ) algorithm BFSHC for PDPHC is given based on the breadth-first search, where σ is the formula size of a given set of Horn clauses. For MASHC, it is shown that the problem is NP-complete, and an O(σ) approximation algorithm FMAS is given. Its experimental evaluation is also presented.