LPAR-16 Accepted Papers with Abstracts

Abstract: By Courcelle"s Theorem we know that any property of finite structures definable in monadic second-order logic (MSO) becomes tractable over structures with bounded treewidth. This result was extended to counting problems by Arnborg et al. and to enumeration problems by Flum et al. Despite the undisputed importance of these results for proving fixed-parameter tractability, they do not directly yield implementable algorithms. Recently, Gottlob et al. presented a new approach using monadic datalog to close the gap between theoretical tractability and practical computability for MSO-definable decision problems. In the current work we show how counting and enumeration problems can be tackled by an appropriate extension of the datalog approach.

Abstract: Pointer analysis statically approximates the heap pointer structure
during a program execution in order to track heap objects or to
establish alias relations between references, and usually
contributes to other analyses or code optimizations.  In recent
years, a number of algorithms have been presented that provide an
efficient, scalable, and yet precise pointer analysis.  However, it
is unclear how the results of these algorithms compare to each other
semantically.

In this paper, we present a general region type system for a
Java-like language and give a formal soundness proof.  The system is
subsequently specialised to obtain a platform for embedding the
results of various existing context-sensitive pointer analysis
algorithms, thereby equipping the computed relations with a common
interpretation and verification.  We illustrate our system by
outlining an extension to a string value analysis that builds on
pointer information.

Abstract: In this paper we introduce an extension of propositional logic that allows clauses to be weighted with values from a generic semiring. The main interest of this extension is that different instantiations of the semiring model different interesting computational problems such as finding a model, counting the number of models, finding the best model with respect to an objective function, finding the best model with respect to several independent objective functions, or finding the set of pareto-optimal models with respect to several objective functions.

Then we show that this framework unifies several solving techniques and, even more importantly, rephrases them from an algorithmic language to a logical language. As a result, several solving techniques can be trivially and elegantly transferred from one computational problem to another. As an example, we extend the basic DPLL algorithm to our framework producing an algorithm that we call SDPLL. Then we enhance the basic SDPLL in order to incorporate the three features that are common in all modern SAT solvers: backjumping, learning and restarts.

As a result, we obtain an extremely simple algorithm that captures, unifies and extends in a well-defined logical language several techniques that are valid for arbitrary semirings.

Abstract: This experimental paper describes the implementation and
evaluation of a static nullness analyser for monothreaded
Java and Java bytecode programs, built inside the julia tool.
Nullness analysis determines, at compile-time, those program points where
the null value might be dereferenced, leading to
a run-time exception. In order to improve the quality of
software, it is hence important to prove that such
situation does not occur.
Our analyser is based on a denotational abstract interpretation of
Java bytecode through Boolean logical formulas, strengthened
with a set of denotational and constraint-based
supporting analyses for locally non-null fields
and full arrays and collections. The complete
integration of all such analyses results in a correct
system of very high precision whose time of analysis remains in the
order of minutes, as we show with some examples of analysis
of large software.

Abstract: We study strategy improvement algorithms for mean-payoff and parity games. We
describe a structural property of these games that has a deep link with the
behaviour of strategy improvement, and we show how awareness of these structures
can be used to accelerate strategy improvement algorithms. We call our
algorithms non-oblivious because they remember properties of the game that they
have discovered in previous iterations. We show that non-oblivious strategy
improvement algorithms perform well on examples that are known to be hard for
oblivious strategy improvement. Hence, we argue that previous strategy
improvement algorithms fail because they ignore the structural properties of the
game that they are solving.

Abstract: We consider a mild extension of universal algebra in which terms are
built both from deterministic and probabilistic variables, and hence
interpreted as distributions.  We prove soundness and completeness of
a proof system for equational reasoning and we provide sufficient
conditions for deciding the validity of a system of
equations.

We illustrate the applicability of our formalism in cryptographic
proofs, showing how it can be used to prove standard equalities such
as optimistic sampling and one-time padding as well as non-trivial
equalities for standard schemes such as OAEP.

Abstract: A rational and selfish environment may have an incentive to cheat
the system it interacts with. Cheating the system amounts to
reporting a stream of inputs that is different from the one
corresponding to the real behavior of the environment. The system
may cope with cheating by charging penalties to cheats it detects.
In this paper, we formalize this setting by means of weighted
automata and their resilience to selfish environments. Automata have
proven to be a successful formalism for modeling the on-going
interaction between a system and its environment. In particular,
weighted automata (WFAs), which assign a cost to each input word,
are useful in modeling an interaction that has a quantitative
outcome. Consider a WFA $\A$ over the alphabet $\Sigma$. At each
moment in time, the environment may cheat $\A$ by reporting a letter
different from the one it actually generates. A penalty function
$\eta:\Sigma \times \Sigma \rightarrow \R^{\geq 0}$ maps each possible
false-report to a penalty, charged whenever the false-report is
detected. A detection-probability function $p:\Sigma \times \Sigma
\rightarrow [0,1]$ gives the probability of detecting each
false-report. We say that $\A$ is $(\eta,p)$-resilient to cheating
if $(\eta,p)$ ensures that the minimal expected cost of an input
word is achieved with no cheating. Thus, a rational environment has
no incentive to cheat $\A$.

We study the basic problems arising in the analysis of this setting.
In particular, we consider the problem of deciding whether a given
WFA $\A$ is $(\eta,p)$-resilient with respect to a given penalty
function $\eta$ and a detection-probability function $p$; and the
problem of achieving resilience with minimum resources, namely,
given $\A$ and $\eta$, finding the minimal (with respect to
$\sum_{\sigma,\sigma"}\eta(\sigma,\sigma")\cdot p(\sigma,\sigma")$)
detection-probability function $p$, such that $\A$ is $(\eta,p)$-resilient.
While for general WFAs both problems are shown to be PSPACE-hard, we present
polynomial-time algorithms for deterministic WFAs.

Abstract: We present ABC, a software tool for automatically computing symbolic upper bounds on the number of iterations of program loops. The system combines static analysis of programs with symbolic summation techniques to derive loop invariant relations among program variables. Iteration bounds are obtained from the inferred invariants, by substituting variables with their greatest values.
We have successfully applied ABC to a large number of examples. The derived symbolic bounds express non-trivial polynomial relations over loop variables. We also report on results to automatically infer symbolic expressions over harmonic numbers as upper bounds on loop iteration counts.

Abstract: In automated synthesis, we transform a specification into a system
that is guaranteed to satisfy the specification. In spite of the rich
theory developed for temporal synthesis, little of this theory has
been reduced to practice. This is in contrast with model-checking
theory, which has led to industrial development and use of formal
verification tools. We address this problem here by considering a
certain class of PSL properties; this class covers most of the
properties used in practice by system designers. We refer to this
class as the class of trigger properties.

We show that the synthesis problem for trigger properties is more
amenenable to implementation than that of general PSL properties.
While the problem is still 2EXPTIME-complete, it can be solved using
techniques that are significantly simpler than the techniques used in
general temporal synthesis. Not only can we avoid the use of Safra"s
determinization, but we can also avoid the use of progress
ranks. Rather, the techniques used are based on classical subset
constructions.  This makes our approach amenable also to symbolic
implementation, as well as an incremental implementation, in which the
specification evolves over time.

Abstract: We present a sound and complete class of models for lambda-calculus
reduction, based on structures inspired by modal logic (the models are very nearly Kripke structures).  Using the models we construct a sound and complete logic, and we identify lambda-terms with certain simple sentences (predicates) by direct compositional translation into the logic.  Under this identification, reduction becomes identified with logical entailment.

Thus, the models suggest a new way to identify logic and computation: both have elementary and concrete representations in our models, and where these representations overlap, they coincide.

In a concluding speculation we note an `intended" subclass of the models, which seems to play a role for our semantics that is analogous to that played by the `intended" cumulative hierarchy models of axiomatic set theory, or the `intended" natural numbers model of formal arithmetic.

Abstract: In this paper we propose proof systems for the intuitionistic modal logic IS5 without labels  and based on a new multi-contextual sequent structure appropriate to deal with such a logic. We first give a label-free natural deduction system and derive from this system, natural deduction systems for the classical modal logic
S5 and also an intermediate logic WS5.
By the Curry-Howard isomorphism, we propose a term calculus, without labels, having good properties (subject reduction, strong normalization). Moreover we propose a label-free sequent calculus for IS5 and prove its soundness and completeness. The study of this calculus leads to a decision procedure for IS5 and thus to an alternative syntactic proof of its decidability.

Abstract: We present a novel way for solving quantifier-free non-linear
arithmetic over (genuine) real domains by a reduction to SAT and
evaluate our approach on different test benches.
To obtain a testbed from termination analysis of rewriting we
generalize matrix interpretations to admit non-negative real
coefficients. The corresponding constraints are solved with our tool
MiniSmt.

Abstract: Disunification is an extension of unification to first-order formulas over syntactic equality atoms. Instead of considering only syntactic equality, I extend a disunification algorithm by Comon and Delor to ultimately periodic interpretations, i.e. minimal many-sorted Herbrand models of predicative Horn clauses and, for some sorts, equations of the form $s^m(x) = s^n(x)$. The extended algorithm is terminating and correct for ultimately periodic interpretations over a finite signature and gives rise to a decision procedure for the satisfiability of equational formulae in ultimately periodic interpretations.

As an application, I show how to apply disunification to compute the completion of predicates with respect to an ultimately periodic interpretation. Such completions are a key ingredient to several inductionless induction methods.

Abstract: State-of-the-art automated theorem provers (ATPs) are today able to solve relatively complicated mathematical problems. But as ATPs become stronger and more used by mathematicians, the length and human unreadability of the automatically found proofs become a serious problem for the ATP users. One remedy is automated proof shortening by invention of new definitions.
This paper proposes a new algorithm for automated shortening of arbitrary terms (like mathematical proofs) by invention of new definitions. It is conjectured that the problem of finding the most shortening definition is NP-complete, and a heuristics based on substitution trees is proposed. The proposed algorithm has been implemented and tested on several automatically found proofs. The results of the tests are included.

Abstract: We investigate the complexity of preorder checking when the specification
is a flat finite-state system whereas the implementation is either a non-flat
finite-state system or a standard timed automaton. In both cases, we show that
simulation checking is EXPTIME-hard, and for the case of a non-flat implementation,
the result holds even if there is no synchronization between the parallel
components and their alphabets of actions are pairwise disjoint. Moreover, we
show that the considered problems become PSPACE-complete when the specification
is assumed to be deterministic. Additionally, we establish that comparing a
flat system and a synchronous non-flat system with no hiding is PSPACE-hard for
any relation lying in between trace containment and bisimulation equivalence.

Abstract: Abstract interpretation provides a practical approach to verifying properties of infinite-state systems. We apply the framework of abstract interpretation to derive an abstract semantic function for the modal $\mu$-calculus, which is the basis for abstract model checking. The abstract semantic function is constructed directly from the standard concrete semantics together with a Galois connection between the concrete state-space and an abstract domain.  There is no need for mixed or modal transition systems to abstract arbitrary temporal properties, as in previous work in the area of abstract model checking. Using the modal $\mu$-calculus to implement CTL,  the abstract semantics gives an over-approximation of the set of states in which an arbitrary CTL formula holds.  Then we show that this leads directly to an effective implementation of an abstract model checking algorithm for CTL using abstract domains based on linear constraints. The implementation of the abstract semantic function makes use of an SMT solver.  We describe an implemented system for proving properties of linear hybrid automata and give some experimental results.

Abstract: We introduce pairwise cardinality networks, networks of comparators,
  derived from pairwise sorting networks, which express cardinality
  constraints.

  We show that pairwise cardinality networks are superior to the
  cardinality networks introduced in previous work which are derived
  from odd-even sorting networks.

  Our presentation identifies the precise relation between odd-even
  and pairwise sorting networks. This relation also clarifies why
  pairwise sorting networks have significantly better propagation
  properties for the application of cardinality constraints.

Abstract: Recently, temporal logics such as mu-calculus and
Computational Tree Logic, CTL, augmented with graded modalities
have received attention from the scientific community,
both from a theoretical side and from an applicative perspective.
Graded modalities enrich
the universal and existential quantifiers with the
capability to express the concept of "at least k" or
"all but k", for a non-negative integer k.
Both mu-calculus and CTL naturally apply as specification languages
for "closed" systems:
in this paper, we study how graded modalities may affect specification
languages for "open" systems. We extend the Alternating-time
Temporal Logic (ATL),
a derivative of CTL interpreted on game structures,
rather than transition systems.

We present, and compare with each other, three different semantics.
We first consider a natural interpretation which
seems suitable to off-line synthesis applications and then we restrict it
to the case where players can only employ memoryless strategies.
Finally, we strengthen the logic by means of a different interpretation
which may find application in the verification of fault-tolerant controllers.
For all the interpretations, we efficiently solve
the model-checking problem both in the concurrent and turn-based
settings, proving its PTIME-completeness.
To this aim we also exploit also a characterization of the maximum
grading value of a given formula.

Abstract: We present an explicitly typed lambda calculus "a la Church" based
  on the union and intersection types discipline; this system is the
  counterpart of the standard type assignment calculus "a la Curry".
  Our typed calculus enjoys Subject Reduction and confluence, and typed
  terms are strongly normalizing when the universal type is omitted.
  Moreover both type checking and type reconstruction are decidable. In
  contrast to other typed calculi, a system with union types will fail
  to be "coherent" in the sense of Tannen, Coquand, Gunter, and Scedrov:
  different proofs of the same typing judgment will not necessarily have
  the same meaning.  In response, we introduce a decidable notion of
  equality on type-assignment derivations inspired by the equational
  theory of bicartesian-closed categories.

Abstract: We describe a technique and a tool called Qex for generating input tables and parameter values for a given parameterized SQL query.  The evaluation semantics of an SQL query is translated into a specific background theory for a satisfiability modulo theories (SMT) solver as a set of equational axioms.  Symbolic evaluation of a goal formula together with the background theory yields a model from which concrete tables and values are extracted.  We use the SMT solver Z3 in the concrete implementation of Qex and provide an evaluation of its performance.

Abstract: Je\v r\"abek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudl\"ak about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Je\v r\"abek"s result: we give a quasipolynomial-time cut-elimination procedure in propositional-logic deep inference. The main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.

Abstract: Grounding is the task of reducing a first order for-
mula to an equivalent propositional formula, and
is important in many kinds of problem solving and
reasoning systems. One method for grounding is
based on an extension of the relational algebra, ex-
ploiting the fact that grounding over a given do-
main is similar to query answering. In this paper,
we introduce two methods for speeding up alge-
braic grounding by reducing the size of tables pro-
duced. One method employs re-writing of the for-
mula before grounding, the other a further exten-
sion of the algebra that makes negation efficient.
We give conditions under which the latter method
is more powerful than the former. We have imple-
mented the methods, and present experimental evi-
dence of their effectiveness.

Abstract: Temporal logics are a well investigated formalism for the specification, verification, and synthesis of reactive systems. Within this family, alternating temporal logic, ATL*, has been introduced as a useful generalization of classical linear- and branching-time temporal logics by allowing temporal operators to be indexed by coalitions of agents. Classically, temporal logics are memoryless: once a path in the computation tree is quantified at a given node, the computation that has led to that node is forgotten. Recently, mCTL* has been defined as a memoryful variant of CTL*, where path quantification is memoryful. In the context of multi-agent planning, memoryful quantification enables agents to "relent" and change their goals and strategies depending on their past history. In this paper, we define mATL*, a memoryful extension of ATL*, in which a formula is satisfied at a certain node of a path by taking into account both the future and the past. We study the expressive power of mATL*, its succinctness, as well as related decision problems. We also investigate the relationship between memoryful quantification and past modalities and show their equivalence. We show that both the memoryful and the past extensions come without any computational price; indeed, we prove that both the satisfiability and the model-checking problems are 2EXPTIME-COMPLETE, as they are for ATL*.

Abstract: Traditionally, the full verification of a program"s functional
correctness has been obtained with pen and paper or with interactive
proof assistants, whereas only reduced verification tasks, such as
extended static checking, have enjoyed the automation offered by
satisfiability-modulo-theories (SMT) solvers.  More recently,
powerful SMT solvers and well-designed program verifiers are
starting to break that tradition, thus reducing the effort involved
in doing full verification.

This paper gives a tour of the language and verifier Dafny, which
has been used to verify the functional correctness of a number of
challenging pointer-based programs.  The paper describes the
features incorporated in Dafny, illustrating their use by small
examples and giving a taste of how they are coded for an SMT solver.
As a larger case study, the paper shows the full functional
verification of the Schorr-Waite algorithm in Dafny.

Abstract: A meta-program is a program that generates or manipulates another
program; in homogeneous meta-programming, a program may generate new
parts of, or manipulate, itself. Meta-programming has been used
extensively since macros were introduced to Lisp, yet we have little
idea how formally to reason about meta-programs. This paper provides
the first program logics for homogeneous meta-programming -- using a
variant of MiniML$_e^{\square}$ by Davies and Pfenning as the
underlying meta-programming language.  We show the applicability of
our approach by reasoning about example meta-programs from the
literature. We also demonstrate that our logics are relatively
complete in the sense of Cook, enable the inductive derivation of
characteristic formulae, and capture exactly the observational
properties induced by the operational semantics.

Abstract: The careful introduction of cut inferences can be used to structure and possibly compress formal sequent calculus proofs. This paper presents CIRes, an algorithm for the introduction of atomic cuts based on various modifications and improvements of the CERes method, which was originally devised for efficient cut-elimination. It is also demonstrated that CIRes is capable of compressing proofs, and the amount of compression is shown to be exponential in the length of proofs.

Abstract: In the celebrated G\"odel Prize winning papers, Herlihy, Shavit, Saks and
Zaharoglou gave topological characterization of waitfree computation.
In this paper, we characterize waitfree communication logically.
First, we give an intuitionistic epistemic logic \kv for asynchronous
communication.  The semantics for the logic \kv is an abstraction of
Herlihy and Shavit"s topological model. In the same way Kripke model
for intuitionistic logic informally describes an agent increasing its
knowledge over time, the semantics of \kv describes multiple agents
passing proofs around and developing their knowledge together.
On top of the logic \kv\kern -3pt, we give an axiom type that characterizes
sequential consistency on shared memory. The advantage of intuitionistic
logic over classical logic then becomes apparent as the axioms for
sequential consistency are meaningless for classical logic because they
are classical tautologies. The axioms are similar to  the axiom type for
prelinerilty $(\varphi\supset\psi)\vee(\psi\supset\varphi)$.
This similarity reflects the analogy between sequential consistency for
shared memory scheduling and linearity for Kripke frames: both require
total order on schedules or models. Finally, under sequential consistency,
we give soundness and completeness between a set of logical formulas called
waitfree assertions and a set of models called waitfree schedule models.

Abstract: The authors of [MT05] proposed a declarative constraint programming framework based on classical
logic extended with non-monotone inductive definitions. In the framework, a problem instance is a finite
structure, and a problem specification is a formula defining the relationship between an instance and its
solutions. Thus, problem solving amounts to expanding a finite structure with new relations, to satisfy
the formula.

We present here the complexities of model expansion for a number of logics, alongside those of
satisfiability and model checking. As the task is equivalent to witnessing the existential quantifiers in
∃SO model checking, the paper is in large part of a survey of this area, together with some new results.
In particular, we describe the combined and data complexity of FO(ID), first-order logic extended with
inductive definitions [DT08] and the guarded and k-guarded logics of [AvBN98] and [GLS01].

Abstract: We build on an existing a term-sequent logic for the
lambda-calculus. We formulate a general sequent system that fully
integrates lambda-reductions between untyped lambda-terms
into first order logic.

We present a cut-elimination result and then offer an application
of cut-elimination by giving a notion of uniform proof for
lambda-terms. We suggest how this allows us to view the calculus of
untyped lambda-reductions as a logic programming
language.

Abstract: The SAT problem is shown to be the first decision NP-complete problem
(Cook,71). It is  central in complexity theory. In the last decade,
the satisfiability proof  procedures are  improved by  symmetry
elimination. A CNF formula usually contains an interesting number of
symmetries. There are two kinds of symmetry exploitation. The first
one corresponds to global symmetry breaking, that is, only the
symmetries of the initial problem (the problem at the root of the
search tree) are detected and eliminated. The second one deals with
all local symmetries that appear  at each node of the search tree. Local symmetry has to be detected and eliminated dynamically during the search. Exploiting such symmetries seems to be a hard task.  Almost all of the known works on symmetry in satisfiability are on global symmetry. Only few works are carried on local symmetry, despite their importance in practice.  An important challenge is then to detect and break local symmetries efficiently during the search.
The work that we present here is a contribution towards an answer to this hard challenge. We present a new method for  local symmetries breaking that consists in detecting dynamically local symmetries by reducing the remaining partial SAT instance at each node of the search tree to a graph that has an equivalent  automorphism group than the symmetry group of the partial SAT instance. We  used the software Saucy to compute the automorphism group and implemented a local symmetry cut in a SAT solver. We experimented this method on several SAT instances and compared it with a method exploiting global symmetries. The results obtained are very promising. Local symmetry improves global symmetry on some hard instances and is complementary to global symmetry.

Abstract: Classical modal logics, based on the neighborhood semantics of Scott and Montague, provide a generalization of the familiar normal systems based on Kripke semantics. This paper defines AGM revision operators on several first-order monotonic modal correspondents, where each first-order correspondence language is defined by Marc Pauly’s version of the van Benthem characterization theorem for monotone modal logic. A revision problem expressed in a monotone modal system is translated into first-order logic, the revision is performed, and the new belief set is translated back to the original modal system. An example is provided for the logic of Risky Knowledge that uses modal AGM contraction to construct counter-factual evidence sets in order to investigate robustness of a probability assignment given some evidence set. A proof of correctness is given.

Abstract: In the Evidential Probability (EP) (Kyburg and Teng 2001) framework, interval-valued probabil- ities are assigned to events given a knowledge base containing statements about logical relationships of classes of objects as well as statements about relative frequencies pertaining to some of those classes. We are interested in the robustness of this inference with respect to perturbations in the given knowledge base. First we define how changes to a (non-deductively-closed) knowledge base are to be carried out by constructing revision and contraction operators that satisfy the AGM pos- tulates, and then we discuss some conditions and measures of robustness. We appeal to a result in (Kyburg and Teng 2002) that allows a logic of risky knowledge based on EP to be characterized by the classical modal system EMN, and define AGM operators for EP through a mapping from monotone neighborhood modal structures to polymodal Kripke structures that admit a first-order correspondent.

Abstract: Grounding is the creation of a propositional formula equivalent to a given first order formula. The formula may be viewed as a specification of a search problem in an abstract modelling language for combinatorial search problems. Efficient grounding algorithms would help  in solving  such problems effectively and make advanced solver technology (such as SAT) accessible to a wider variety of users. One promising method for grounding is based on the relational algebra from the field of Database research. We have added arithmetic and aggregates to the syntax and extended the original grounding algorithm to be able to handle these structures, too. To do so, we used a method which allows us to choose a particular representation for aggregates. Here, we describe the six representations we have used to convert count aggregate to SAT. We compared the performance of these encodings both theoretically and experimentally. The results show that each of them performs the best in some cases and this motivates us to use an automatic approach to select the best encoding at running time.

Abstract: Basin and Ganzinger [2001] have proved that for finite sets of clauses saturated for ordered resolution, the ground entailment problem is order local. This implies decidability of ground entailment problems when the employed ordering has a finite complexity. We present in this paper an extension of that result that does not assume finite complexity of the ordering.

Abstract: In previous papers, results about capturing the complexity class NP with the model expansion task for languages with built-in arithmetic have been demonstrated. The purpose of this paper is to show the implications of those results to the practice of KR, and to two languages, ASP and IDP in particular. In addition, we describe a logic which we call PBINT and  show that PBINT provides a good basis for an attractive modelling language. We demonstrate that PBINT allows for compact and natural encodings and it can be supported with efficient implementation techniques.

Abstract: Description logic (DL) reasoners generally handle axioms by absorption that rewrites axioms into forms suitable for lazy unfolding. However, absorption techniques are employed in a mostly uniform way regardless of the characteristics of an input knowledge base. The overall effectiveness of axiom absorption remains to be improved, particularly when a large quantity of complex axioms are present, which is well beyond the capability of any single absorption technique.

To ameliorate absorption techniques, this paper presents a framework applying AI planning to axiom absorption. In this framework, a state space planner is used to encode state-of-the-art absorption techniques. The planner first applies appropriate absorptions to axioms, then it produces a plan that automatically organizes absorption techniques in a certain sequence to maximize the number of axioms to be absorbed. Compared to a predetermined or fixed order of applying absorption techniques, the proposed framework tends to be more flexible and effective.