# parameterized_logical_theories__2002aafb.pdf

Parameterized Logical Theories

Fangzhen Lin Department of Computer Science & HKUST-Xiaoi Joint Lab The Hong Kong University of Science and Technology Clear Water Bay, Kowloon, Hong Kong flin@cs.ust.hk

A theory in first-order logic is a set of sentences. A parameterized theory is a first-order theory with some of its predicates and functions identified as parameters, together with some import statements that call other parameterized theories. A KB is then a collection of these interconnected parameterized theories, similar to how a computer program is constructed as a set of functions in a modern programming language. In this paper, we provide a translational semantics for these parameterized theories in first-order logic using the situation calculus. We also discuss their potential uses in areas such as multi-context reasoning and logical formalization of computer programs.

Introduction In AI, first-order logic and its variants have been widely used in KR. Central to this use is the construction of a KB, which is normally a logical theory, i.e. a set of sentences, for the domain of interest. When the domain of interest is complex and diverse, it is often desirable to organize its KB in some modular ways. A simple approach is to organize it as a hierarchy of smaller ones (e.g. (Hendrix 1975; Carnegie Group 1985; Lenat 1995; Lifschitz and Ren 2006)). The hierarchy can be in terms of refinement, abstraction, or some input/output relationship. Another approach is to treat the KB as a collection of contexts that are connected by some meta-axioms or rules to connect these contexts (e.g. (Mc Carthy 1993; Giunchiglia 1993; Giunchiglia and Serafini 1994; Mc Carthy and Buva c 1997; Br ezillon 1999; Ghidini and Giunchiglia 2001)). In this paper, we propose a notion of parameterized theories and consider a KB to be a collection of such theories. Informally, a parameterized theory is like a first-order theory but with some of the predicate and function symbols in it identified as parameters, and these parameters can be replaced when called from another theory. Like contexts, there are no built-in hierarchies in our framework. Unlike contexts, there are no separate meta-axioms or rules. As we will see, to connect some parameterized theories, one can define a new one that calls these theories. In a sense, parameterized theories are like functions in computer programming languages: they can call and be

Copyright 2021, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

called by others. In fact, our motivation for this work came from a recent work by Lin (2016) that translates a procedural program to a first-order theory. While trying to extend Lin s approach to more complex programs, including those involving functions with side effects, we encountered the need for embedding a logical theory inside another one, for the reason that if a function P in a program is formalized as a logical theory, then when another function Q calls P, there must be a way for the theory of Q to access the theory of P. We will outline how our notion of parameterized theories can be used to address this issue. The rest of the paper is organized as follows. In the next section, we define the syntax of parameterized theories, and illustrate it with examples. We then propose a formal semantics that translates a set of parameterized theories to a set of first-order theories in the situation calculus, by viewing theory calls as actions. This is the main technical contribution of the paper. We next describe some possible applications, discuss related work, and then conclude the paper.

Parameterized Theories

We consider parameterized theories in first-order logic. Each parameterized theory can have its own language which is a set of function (including constant) and predicate symbols. We use lambda notation to denote anonymous functions and relations. A lambda expression is one of the form λx1...λxk.E, where E is either a term or a formula that has x1, .., xk as the free variables. If E is a term, then it defines a k-ary function. If it is a formula then it defines a k-ary predicate. For example, if f is a binary function and g a unary function, then λx.f(x, g(x)) is an anonymous unary function defined by the following equation:

y.(λx.f(x, g(x)))(y) = f(y, g(y)).

Similarly, if P is a binary predicate, then λx. y P(x, y) is an anonymous unary predicate such that (λx. y P(x, y))(z) is true iff y P(z, y) is true. As we mentioned, a parameterized theory is essentially a first-order theory with some of the functions and predicates in it designated as parameters that can be replaced when it is called or imported into another theory.

Definition 1. Given a language L, a parameterized theory C(p1, ..., pn) consists of a unique name C, a tuple

The Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI-21)

(p1, .., pn) of formal parameters, which are distinct predicate and function symbols in L, and a set of axioms which are either first-order sentences in L or import statements of the form C (t1, ..., tm), (1)

C is a parameterized theory with some formal parameters q1, ..., qm; t1, ..., tm, called the actual parameters, are expressions (terms, functions, predicates, or lambda expressions) of the same types as q1, ..., qm, respectively.

Notice that the qi s are in the language of C (the callee), and ti s in the language of C, the caller. One can read the import statement (1) as: import C with each formal parameter qi replaced by the actual one ti, 1 i m.

In the following, we use the following format

Parameterized Theory C(p1, ..., pn) : ϕ1, ... ϕm

to define a parameterized theory whose name is C, whose parameters are p1, ..., pn, and whose axioms are ϕ1, ..., ϕm. Unless otherwise stated, the language of this theory is taken to be the set of function and predicate symbols that are mentioned in the first-order axioms of the theory. We also use the convention that free variables in a displayed formula are universally quantified from outside so for example, P(x) Q(x)

stands for x.P(x) Q(x).

Example 1 The following is a parameterized theory for a syllogism, a generalization of modus ponens:

Parameterized Theory Syllogism(a, prem, concl):

prem(a), prem(x) concl(x),

where a is a constant symbol and a parameter of the parameterized theory, and x is a variable, thus universally quantified from outside.

This is a base (primitive) parameterized theory that has no import statements. The following parameterized theory uses Syllogism. It has an import statement but no first-order axioms of its own:

Parameterized Theory Socr Syll():

Syllogism(Socrates, man, mortal),

where Socrates is a constant, and man and mortal unary predicates. One can expect that parameterized theory Syllogism will entail concl(a), and as a result, Socr Syll() will entail mortal(Socrates).

A parameterized theory can call another one multiple times. For example, the following import statements can all be in the same parameterized theory:

Syllogism(Socrates, man, mortal), Syllogism(Xenophon, man, mortal), Syllogism(Tweety, bird, fly).

There is also no guard against inconsistent calls, like:

Syllogism(Tweety, bird, fly), Syllogism(Tweety, penguin, λx. fly(x)).

Example 2 Parameterized Theories can call each other, like mutually recursive functions. The following is a trivial example on a language with only propositional symbols (0-ary predicates). Parameterized Theory Prop1(p): Prop2(p). Parameterized Theory Prop2(p): Prop1( p). It may appear that these two mutually recursive calls will result in a contradiction. But if one follows the call chain: Prop2(p) Prop1( p) Prop2( p) ..., it is more like a loop that never terminates. We ll see that under our semantics, these two theories are the same as tautology.

Semantics Given a parameterized theory C(p1, ..., pn), a symbol in its language is called a local symbol if it is not a parameter. Local symbols are supposed to be existentially quantified. For example, given

C(p) : p q,

the following two calls to it in another parameterized theory:

C (r) : C(r), C( r)

should not lead to a contradiction as the local symbol q is supposed to be existentially quantified. For example, C (r) in this case can be formalized as

q(r q) q( r q), (2)

which is a tautology. In general, local symbols can be functions and predicates. Quantifying over them will lead to second-order axioms. Instead of existential quantification, we can introduce a fresh new name for each local symbol every time a parameterized theory is called. For example, C (r) can also be formalized as (r q1) ( r q2). (3) Notice that (2) and (3), while not equivalent in general, are equivalent if restricted to the language of C : forgetting about q1 and q2 in (3) (Lin and Reiter 1994) also yields tautology. In this paper we adopt the renaming approach, and propose a systematic way of renaming parameters and local symbols by introducing special situation objects to bookmark parameterized theory calls. The idea is similar to how function calls are implemented in programming languages

with so called activation records. Of course, we do not use these data structures. Our semantics is entirely declarative. We begin by adding a new situation sort S to the language. Variables of this sort will be named using s, like s, s , s1 etc. Unary functions from S to S will be named using µ, like µ, µ , µ1 etc. These unary functions are the ones that will be used to bookmark parameterized theory calls, as we will see shortly. For those familiar with the situation calculus (Mc Carthy 1968; Reiter 2001; Lin 2007), these unary functions are like actions. We assume a special constant S0, the dummy situation from which new situations are created using unary functions µ1, µ2, etc. Given a symbol p( x) in the language of a parameterized theory, we extend it with a sort S argument. Informally p( x, s) denotes the value of p( x) inside the parameterized theory that is called in situation s. This way of extending a predicate or function with a new situation argument is standard in the situation calculus. Our proposed semantics maps a parameterized theory C to two sets of axioms: one for reasoning within the parameterized theory and the other for reasoning about the parameterized theory when it is called. We call the first set the primary theory of C and denote it by PT(C). We call the the latter the situational theory of C and denote it by ST(C). We now describe how to construct these two sets. To simplify our notation, without loss of generality, we assume that there is no overlap between the languages of any two different parameterized theories. This can be achieved by symbol renaming using a uniform scheme like adding a unique name as the prefix to every symbol in a parameterized theory. Intuitively, the primary theory of C is just the normal firstorder axioms in it, plus when there is an import statement in it, the axioms that pass the actual parameters to the called theory by creating a unique calling context: Definition 2 (Primary Theory of a Parameterized Theory). Given a parameterized theory C, its primary theory PT(C) consists of the first-order axioms in C and for each import statement C (t1, ..., tn) in it with the prototype C (p1, ..., pn), the following axioms:

x.ti( x) .= pi( x, µ(S0)), 1 i n, (4)

where µ : S S is a new unary function introduced for this call, and ti .= pi is ti = pi if pi is a function, and t1 pi if pi is a predicate. The situational theory of C, written ST(C), is obtained from its primary theory by extending all symbols in C with a situation argument s and universally quantifying over it from the outside. Definition 3 (Situational Theory of a Parameterized Theory). Given a parameterized theory C, ST(C) is defined as follows:

ST(C) = { s.ϕ[s] | ϕ PT(C)}, (5)

where ϕ[s] is obtained from ϕ by the following substitutions: Replace S0 by s; for each symbol p, replace its every occurrence p( t) by p( t, s), where t does not contain sort S.

Intuitively, ϕ[s] means ϕ holds in s, and is applied only to a formula ϕ that does not mention any other situation term except S0. For example, (f(a, g(b, S0)) = f(c, x))[s] is

f(a(s), g(b(s), s), s) = f(c(s), x, s),

assuming a, b, and c are constants, g and f functions, and x a variable. Given a collection of parameterized theories, its semantics is then the union of the translated theories of all the parameterized theories in the collection. However, when reasoning about a specific parameterized theory, there is no need to consider all other theories, only those that may potentially be called by it. Given a parameterized theory C, we say that C depends on C if C calls C or C calls a parameterized theory C such that C depends on C , i.e. the transitive closure of C calls C . Given a C, let

Dep(C) = {C | C depends on C }.

Notice that it is possible for C Dep(C) for some C. Definition 4. Let C be a parameterized theory. The translated theory of C, written Σ(C), is defined as the following first-order theory:

Σ(C) = PT(C) ST(C) [

C Dep(C) (PT(C ) ST(C ))

In the following we consider the semantics of C to be Σ(C). For example, we say that C is a consistent parameterized theory if Σ(C) is a consistent first order theory. We say that C entails a sentence ϕ, written C |= ϕ by overloading the classic entailment symbol |= , if Σ(C) |= ϕ in first-order logic. The following theorem says that for reasoning about sentences in the langauge of C, we only need PT(C) and ST(C ) from those C that C depends on. Theorem 1. Let C be a parameterized theory and ϕ a sentence in C. We have that

Σ(C) |= ϕ iff T (C) |= ϕ,

T (C) = PT(C) [

C Dep(C) ST(C )

Proof. The if direction is trivial. We show the only if part. Suppose T (C) |= ϕ is not true, and M is a model that satisfies T (C) but not ϕ. From M, we construct a model M that satisfies Σ(C) but not ϕ. Notice that a symbol p in a language has two versions: its original one and the extended one p(s). M has the same domains as M. For each p, there are two cases:

1. p is in C. M interprets p the same as M does. If C Dep(C), then M also interprets p(s) the same as M does. Otherwise, M interprets p(s) the same as p by ignoring the last argument s. 2. p is in a different parameterized theory C . M interprets p(s) the same as M does, and p the same as p(S0).

Under this construction, one can verify that M is a model of Σ(C). It does not satisfy ϕ as M does not. Notice how the unique role that S0 plays in the construction of M .

The following result says that when there is no recursive calls, our semantics works like macro or inline expansions. For simplicity, it s given for the basic case of a theory calling another base theory. Again, without loss of generality, we assume the two theories have no common predicates and functions. Our proof makes use of forgetting, and is omitted here for lack of space.

Theorem 2. Let C( p) and C ( q) be two parameterized theories that do not have overlap in their languages. Suppose C has a single import statement C ( t) and C has no import statement. For any formula ϕ in the language of C, C |= ϕ iff Expand(C) |= ϕ, where Expand(C) is the conjunction of the first-order axioms in C and C , with each qi in q replaced by its corresponding ti in t in the axioms of C .

Examples We now illustrate this translational semantics with some examples from the previous sections. Consider first the following two parameterized theories at the beginning of last section:

C(p) : p q, C (r) : C(r), C( r).

The parameterized theory C has no import statement, so its primary theory, PT(C), is just p q. Its situational theory, ST(C), is s.p(s) q(s). On the other hand, PT(C ), is

r p(µ1(S0)), r p(µ2(S0)),

where µ1 and µ2 are the two unary functions corresponding to the two calls, respectively. ST(C ) is:

r(s) p(µ1(s)), r(s) p(µ2(s)).

Clearly, the union of all these theories is consistent. Furthermore, forgetting p(s), q(s) and r(s) in them will yield p q. This means that the parameterized theory C does not say anything informative.

Syllogism Consider the set of parameterized theories Syllogism and Socr Syll. For the first one, its primary theory is just the set of axioms in it as there are no import statements:

prem(a), prem(x) concl(x).

Its situational theory is obtained by adding a situation argument to all the axioms:

prem(a(s), s), prem(x, s) concl(x, s).

This parameterized theory entails concl(a). It is easy to see that any parameterized theory that calls Syllogism(t, p1, p2) will entail p2(t). For example, Socr Syll calls Syllogism(Socrates, man, mortal), thus entails mortal(Socrates). This can be independently verified as follows. For Socr Syll, its primary theory is:

Socrates = a(µ(S0)), man(x) prem(x, µ(S0)), mortal(x) concl(x, µ(S0)),

where µ is the unary function introduced for the call Syllogism(Socrates, man, mortal). Its situational theory is:

Socrates(s) = a(µ(s)), man(x, s) prem(x, µ(s)), mortal(x, s) concl(x, µ(s)).

The conclusion mortal(Socrates) of Socr Syll can now be verified as it is a logical consequence of ST(Syllogism) PT(Socr Syll), the primary theory of Socr Syll and the situational theory of Syllogism as the former calls the latter. The following is an example of multiple calls that lead to a contradiction:

Syllogism(Tweety, bird, fly), Syllogism(Tweety, bird, λx. fly(x)).

Let µ1 and µ2 be the unary functions for these two calls, respectively. These two calls generate the following axioms:

Tweety = a(µ1(S0)), bird(x) prem(x, µ1(S0)), fly(x) concl(x, µ1(S0)), Tweety = a(µ2(S0)), bird(x) prem(x, µ2(S0)), fly(x) concl(x, µ2(S0)).

They entail both fly(Tweety) and fly(Tweety), a contradiction caused by the two inconsistent calls.

Mutual Recursion Consider now the mutually recursive theories Prop1(p) and Prop2(p) in the last section. First of all, we rename the parameter p to make it unique to each theory.

Prop1(p1) : Prop2(p1), Prop2(p2) : Prop1( p2).

The primary theory for Prop1(p1), PT(Prop1), is

p1 p2(µ1(S0)),

and ST(Prop1) is

p1(s) p2(µ1(s)),

where µ1 is the unary function corresponding to the call Prop2(p1). Similarly PT(Prop2) is p2 p1(µ2(S0)), and ST(Prop2) is s. p2(s) p1(µ2(s)), where µ2 is the unary function corresponding to the call Prop1( q2). Thus

p1 p2(µ1(S0)) p1(µ2(µ1(S0))) p2(µ1(µ2(µ1(S0)))) p1(µ2(µ1(µ2(µ1(S0)))))

which is a consistent infinite equivalence chain. In fact, forgetting the two unary predicates p1(s) and p2(s) will result in a tautology, meaning the set of the above sentences has no information about the truth values of p1 and p2. Recursively defined functions and relations are most useful on inductively defined domains. For example, we can define the concepts of odd and even numbers recursively using the following two parameterized theories: Parameterized Theory Odd(odd): Even(tmp1), odd(n) n = 0 tmp1(n 1) Parameterized Theory Even(even): Odd(tmp2), even(n) n = 0 (n > 0 tmp2(n 1)), where we assume a pre-defined natural number domain with built-in functions like - . We will have more to say about sorts and predefined (interpreted) symbols later. As an example, under our semantics, assuming the standard interpretation to these predefined symbols, and letting µ1 be the unary situation function for the call Even(tmp1) in Odd, and µ2 the unary situation function for the call Odd(tmp2) in Even, odd(3) can be deduced as follows: odd(3) temp1(2) even(2, µ1(S0)) temp2(1, µ1(S0)) odd(1, µ2(µ1(S0))) temp1(0, µ2(µ1(S0))) even(0, µ1(µ2(µ1(S0)))) true

Extensions Conditional Imports We have defined an import statement as a wholesome call to a parameterized theory. It can be generalized to include conditional ones such as: penguin(Tweety) Syllogism(Tweety, bird, λx. fly(x)), parrot(Tweety) Syllogism(Tweety, bird, fly). Conditional imports will be needed for formalizing the semantics of computer programs as discussed in the next section. Our semantics can be extended to these conditional calls straightforwardly. For example, the above two example calls will yield the following axioms in the primary theory of the parameterized theory that contains them: penguin(Tweety) Tweety = a(µ1(S0)) x(bird(x) prem(x, µ1(S0))) x( fly(x) concl(x, µ1(S0))), parrot(Tweety) Tweety = a(µ2(S0)) x(bird(x) prem(x, µ2(S0))) x(fly(x) concl(x, µ2(S0))). Their corresponding axioms in the situational theory can then be generated as usual. Import statements, however, should not be used like ordinary predicates. For example, putting a negation in front of them like Syllogism(Tweety, bird, fly) does not seem to make any sense.

Sorts and Interpreted Symbols

So far we have considered first-order languages without multiple sorts and interpreted or pre-defined symbols. However, these additional features can be accommodated without any problem. A first-order many-sorted language (with interpreted symbols) consists of the following components:

A finite set of sorts, some of them marked as interpreted, meaning they will be interpreted by some pre-defined sets.

A finite set of function and predicate symbols. Each of them will come with a type: a function symbol f will have a type of the form τ1 τn τ, and a predicate of the form τ1 τn, where the τ s are sorts. Some of the symbols can be designated as interpreted, meaning their interpretations will be fixed.

Lambda expressions are the same as before but will have types as well. Parameterized theories and import statements are also defined as before, but with the following restriction:

Interpreted symbols cannot be formal parameters.

In an import statement C(t1, ..., tn) that calls C(p1, ..., pn), each actual parameter ti must be of the same type as its corresponding formal parameter pi.

The semantics for these parameterized theories is the same as before. We have seen earlier that the two mutually recursive theories Odd and Even use interpreted sorts and symbols. We give another example here. It uses one interpreted sort N for natural numbers, and one (un-interpreted) sort O for domain objects. We also use + and 0 as interpreted symbols of their usual meaning in N. The following base parameterized theory defines the transitive closure of a binary relation.

Parameterized Theory Trans Clos(base, tr):

tr(x, y) n.tr0(x, y, n), tr0(x, y, 0) base(x, y), tr0(x, y, n + 1) z.base(x, z) tr0(z, y, n),

where x and y are variables of sort O, and n a variable of sort N. They are all universally quantified over their respective sorts. Notice that from the axioms, one can see that base is a binary predicate of sort O O. The types of other predicates can be similarly determined.

Other parameterized theories can use Trans Clos to define transitive closures of some specific binary relations. The following parameterized theory uses Trans Clos to define when a node is reachable from a starting node.

Parameterized Theory Reachable(start, edge, reachable):

Trans Clos(edge, path), reachable(x) path(start, x),

where x is a variable of sort O, and start a constant symbol of sort O.

Figure 1: A magic box

Some Applications Multicontext Reasoning A collection of parameterized theories is a set of logical theories interconnected by import calls. The connection with multicontext reasoning is apparent, at least informally. Consider the magic box shown in Figure 1, an example adapted from (Ghidini and Giunchiglia 2001). There are two agents, Mr. 1 and Mr. 2, who look at the box from two perpendicular sides. Mr. 1, looking into the box from the side, can see whether the left and the right rows of the box have balls. Mr. 2, looking from the bottom, can tell whether the left, center, and the right column of the box have balls. Their knowledge alone cannot determine exactly which cell is occupied. But combining their knowledge, sometimes one can. For example, if Mr. 1 sees a ball on the left side but no ball on the right side, and Mr. 2 sees a ball on the left side, then we can conclude that the top left corner is occupied by a ball. This is a classic example in multi-context systems where contexts are used to represent agents views, and bridge rules for linking contexts to reason about the state of the box. In our framework, we can specify an agent s point of view by a parameterized theory, and use a main parameterized theory to aggregate the views by calling the agents parameterized theories. For the magic box problem, the main parameterized theory can be written as follows:

Mr1(l1, r1), Mr2(l2, c2, r2), l1 b11 b12 b13, r1 b21 b22 b23, l2 b11 b21, c2 b12 b22, r2 b13 b23,

where Mr1() and Mr2() are the parameterized theories for the two agents, respectively. For example, if Mr. 1 sees that the left row is occupied but not the right row, while Mr. 2 sees that the left and the right columns are occupied but not the center one, then we have

Mr1(l, r): l r.

Mr2(l, c, r): l c r. With these three parameterized theories, it is easy to see that the main parameterized theory entails b11 (the top left corner is occupied by a ball).

Program Semantics Our initial motivation for proposing this framework of logical theories is to provide a logical semantics to programming languages. Lin (2016) proposed a translation from programs in a core programming language to first-order theories. Later they demonstrated the practical effectiveness of this approach in automated program verification (Rajkhowa and Lin 2018, 2019), with SOTA performance in a recent program verification competition. However, one limitation with their system is that it has difficulty dealing with functions with side effects. For example, consider a function called Add One(A) that takes an array A of integers as input and adds 1 to every element in it. If arrays are implemented as reference variables like in C, then this function has no effect on the input array variable itself. Instead, it achieves its goal through its side effects of changing the values of a consecutive sequence of locations pointed to by the array variable. One way to axiomatize the effects of this function is to introduce an array sort and use the following two functions, value(a, i) that denotes of the value of the ith element in a one-dimensional array a, and len(a) that denotes the length of the array a. The effect of Add One(A) can then be formalized by the following axioms:

A = A, len (a) = len(a), 1 i len(A) value (A, i) = value(A, i) + 1, 1 i len(a) a = A value (a, i) = value(a, i),

where a is an array variable, and i an integer variable, both are universally quantified. Primed symbols like A denote the outputs of the function. So A and A are the values (locations) of the input array A before and after Add One(A) is executed, respectively. A = A means that the function has no effect on the value of the input array as a reference variable. Similarly, value is value after the function returns, so value (a, i) denotes the value of the ith element of the array object a after the function returns. Now, whenever Add One(A) is called in a program, we will need to insert the above set of axioms when translating the program to a first-order theory. One can imagine the challenge of systematically doing this, especially when a function is recursively defined. This is what motivated us to introduce the notion of parameterized theories in this paper, and also the reason why we propose a translational semantics for these parameterized theories. Each function in a program will now be formalized as a parameterized theory, and a function call will be translated to a corresponding import statement. Notice that in a program, a function call can occurs in an expression such as X=X+f(X) or in a conditional statement like if X==0 then f(X). In the first case, one can eliminate calls in an expression by using a new variable, like

Y=f(X); X=X+Y; (notice that while f(X) may have side effects, it will not have side effect on a value variable like X that occurs in an arithmetic expression). In the latter case, we can extend our import statements to conditional ones of the form ϕ C(t1, ..., t2), where ϕ is a sentence in the language of the caller, as we discussed earlier.

Related Work In a nutshell, a parameterized theory is a named theory with some of its predicates and functions marked as parameters so that it can be called by other theories. This is of course similar to how functions and procedures are defined and used in high level programming languages, except that there is no real computation done when a parameterized theory is called - it is just a way to import a set of axioms. In this sense, calling a parameterized theory is like importing a package or a module in computer programming, except that packages and modules in software engineering do not normally have parameters. In logic, variables that range over predicates and functions are second-order. Thus a parameterized theory could be captured by a third-order predicate with second-order arguments. While we do not intend to use third-order logic for reasoning, we are currently exploring a third-order logic semantics and studing its relationship with our first-order semantics here. There has been much work on various notions of modules and modular systems in KR. In fact, almost every KR formalism, monotonic or nonmonotonic, has seen some work on them. To our understanding, the most closely related work in KR is that on reasoning about contexts (Mc Carthy 1993; Giunchiglia 1993), especially those on multicontext systems (MCS) (e.g. (Giunchiglia 1993; Giunchiglia and Serafini 1994; Ghidini and Giunchiglia 2001; Brewka, Roelofsen, and Serafini 2007; Brewka et al. 2011, 2018)). MCS has been used for aggregating heterogeneous knowledge sources. The basic idea is that each knowledge source will have its own language and axioms, and they are integrated using so-called bridge rules. A classic example that illustrates the uses of the MCS is the magic box example that we discussed earlier. As we have seen, instead of bridge rules, we use a parameterized theory to import all knowledge sources and aggregate them by standard first-order axioms. It s an interesting open question if the two frameworks can be related in a precise way. Given that MCS has been extended to nonmonotonic logics (Brewka, Roelofsen, and Serafini 2007), a good understanding of the relationships between these two frameworks will help when we consider extending parameterized theories to nonmonotonic logics. There are two key points that we can make about our approach. One is that different parameterized theories can assumed to have completely different languages. The other is that theory calls can be recursive, especially when there are pre-interpreted sorts for inductively defined objects. The first point simplifies many issues, like how two modules may interact through shared vocabularies, a common issue for work on modules in many formalisms (e.g. separability in DLs (Konev et al. 2009) and input/output interface in ASP (Janhunen et al. 2009)). The second point is what made this

work non-trivial, especially given that we want a translational first-order semantics. While work on module is often based on computational considerations, our main motivation is on first-order theory composition, especially in the context of logical formalization of programs: if a function is represented by a firstorder theory T, and a program calls this function, then a first-order theory for the program can be computed from T in a modular way. If there is no cycle in the call dependency graph, then this can be handled by macro expansion or inline function. Interestingly, this is the approach taken in (Baral, Dzifcak, and Takahashi 2006) for ASP and in a recent work on programming with logical constraints using socalled knowledge units (Liu and Stoller 2020). However, being able to handle recursive calls is crucial for us. Again, the reason is that when we want to have a one to one correspondence between functions in a computer program and parameterized theories here, a set of recursively defined functions will cause cycles in the chains of theory calls. Notice that Lin (2016) also considered recursive functions. But those functions are assumed to return values without any side effects. In a sense, recursive theory calls are our answer to recursive functions with side effects.

Concluding Remarks

Motivated by the need to have callable theories in logical formalization of computer programs, we have proposed a framework of parameterized first-order theories. While reasoning about parameterized theories appears to require higher-order logics, we have been able to provide a firstorder semantics by making use of the situation calculus. Our semantics is modular, declarative, and at the same time retains certain procedural information of how parameterized theories are run . We have shown some possible applications of our framework in formal semantics of computer programs and in reasoning about contexts. One future work is to implement this framework in program verification, following the work of Rajkhowa and Lin (2018; 2019). Their system was based on a translation (Lin 2016) from programs to first-order theories, and uses the offthe-shelf math system Sym Py as the algebraic simplifier and SMT solver Z3 (de Moura and Bjørner 2008) as the theorem prover. Remarkably, despite its simplicity, their system managed to achieve SOTA performance in the tracks that it competed in at SV-COMP 20191. In particular, it came first in the Arrays subcategory and Recursive subcategory of Reach Safety category of the competition. However, it uses inline expansion when there is a function call with array parameters. With this work, we can implement a more general system that is able to handle recursive functions with array parameters as well as other functions with side effects. We also plan to use the proposed framework in applications other than program verification. We have mentioned multi-context systems. We hope to have more to report on this soon.

1See https://verifierintegerassignment.github.io

Acknowledgments

I want to thank Pritom Rajkhowa for many useful discussions that we had during the course of our work on program verification in first-order logic where the need for this work first arose. I also thank Annie Liu, Yisong Wang, and the anonymous reviewers for their many critical, constructive and helpful comments on earlier versions of this paper. Of course, any remaining problems and possible errors are solely the author s responsibility.

Baral, C.; Dzifcak, J.; and Takahashi, H. 2006. Macros, Macro Calls and Use of Ensembles in Modular Answer Set Programming. In Logic Programming, 22nd International Conference, ICLP 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, 376 390.

Brewka, G.; Eiter, T.; Fink, M.; and Weinzierl, A. 2011. Managed Multi-Context Systems. In Walsh, T., ed., IJCAI 2011, 786 791. IJCAI/AAAI. doi:10.5591/978-1-57735516-8/IJCAI11-138.

Brewka, G.; Ellmauthaler, S.; Gonc alves, R.; Knorr, M.; Leite, J.; and P uhrer, J. 2018. Reactive multi-context systems: Heterogeneous reasoning in dynamic environments. Artif. Intell. 256: 68 104. doi:10.1016/j.artint.2017.11.007.

Brewka, G.; Roelofsen, F.; and Serafini, L. 2007. Contextual Default Reasoning. In Veloso, M. M., ed., IJCAI 2007, 268 273.

Br ezillon, P. 1999. Context in problem solving: a survey. The Knowledge Engineering Review 14(1): 47 80. doi:10. 1017/S0269888999141018.

Carnegie Group. 1985. Knowledge Craft 3.0 reference manual. Volume 1 and 2. Technical report, Carnegie Group Inc, Pittsburgh, Pennsylvania, U.S.A.

de Moura, L.; and Bjørner, N. 2008. Z3: An Efficient SMT Solver. In Ramakrishnan, C. R.; and Rehof, J., eds., Tools and Algorithms for the Construction and Analysis of Systems, 337 340. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-540-78800-3. URL http://research. microsoft.com/en-us/um/redmond/projects/z3/.

Ghidini, C.; and Giunchiglia, F. 2001. Local Models Semantics, or contextual reasoning = locality + compatibility. Artificial Intelligence 127(2): 221 259. doi:https: //doi.org/10.1016/S0004-3702(01)00064-9.

Giunchiglia, F. 1993. Contextual reasoning. Epistemologia 16: 341 364.

Giunchiglia, F.; and Serafini, L. 1994. Multilanguage hierarchical logics or: How we can do without modal logics. Artificial Intelligence 65(1): 29 70.

Hendrix, G. 1975. Expanding the utility of semantic networks through partitioning. In Proc. of IJCAI 75, 115 121.

Janhunen, T.; Oikarinen, E.; Tompits, H.; and Woltran, S. 2009. Modularity Aspects of Disjunctive Stable Models. J. Artif. Intell. Res. 35: 813 857.

Konev, B.; Lutz, C.; Walther, D.; and Wolter, F. 2009. Formal Properties of Modularisation, 25 66. Berlin, Heidelberg: Springer Berlin Heidelberg. ISBN 978-3-642-019074. doi:10.1007/978-3-642-01907-4 3. URL https://doi.org/ 10.1007/978-3-642-01907-4 3. Lenat, D. B. 1995. CYC: A Large-Scale Investment in Knowledge Infrastructure. Commun. ACM 38(11): 32 38. doi:10.1145/219717.219745. Lifschitz, V.; and Ren, W. 2006. A Modular Action Description Language. In Proceedings, AAAI-2006, 853 859. AAAI Press. Lin, F. 2007. Situation Calculus. In van Harmelen, F.; Lifschitz, V.; and Porter, B., eds., Handbook of Knowledge Representation. Elsevier. Lin, F. 2016. A Formalization of Programs in First-Order Logic with a Discrete Linear Order. Artificial Intelligence 235: 1 25. Lin, F.; and Reiter, R. 1994. Forget it! In Greiner, R.; and Subramanian, D., eds., Working Notes of AAAI Fall Symposium on Relevance, 154 159. The American Association for Artificial Intelligence, Menlo Park, CA. Liu, Y. A.; and Stoller, S. D. 2020. Knowledge of Uncertain Worlds: Programming with Logical Constraints. In Proceedings of the 2020 International Symposium on Logical Foundations of Computer Science, volume 11972 of LNCS, 111 127. Deerfield Beach, Florida: Springer. doi: https://doi.org/10.1007/978-3-030-36755-8 8. Mc Carthy, J. 1968. Situations, actions and causal laws. In Minsky, M., ed., Semantic Information Processing, 410 417. MIT Press, Cambridge, Mass. Mc Carthy, J. 1993. Notes on formalizing context. In Proc. of IJCAI 93, 555 560. Mc Carthy, J.; and Buva c, S. 1997. Formalizing context (expanded notes). In Aliseda, A.; van Glabbeek, R.; and Westerst a hl, D., eds., Computing Natural Language, 13 50. CSLI Publications, Stanford. Rajkhowa, P.; and Lin, F. 2018. Extending VIAP to Handle Array Programs. In 10th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018, Oxford, UK, July 18-19. URL https://github.com/Verifier Integer Assignment/svcomp/blob/master/extending-viap-array.pdf. Rajkhowa, P.; and Lin, F. 2019. VIAP 1.1 - (Competition Contribution). In Beyer, D.; Huisman, M.; Kordon, F.; and Steffen, B., eds., Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of Lecture Notes in Computer Science, 250 255. Springer. URL https: //doi.org/10.1007/978-3-030-17502-3\ 23. Reiter, R. 2001. Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems. The MIT Press.