{'fraction_non_alphanumeric': 0.050327062522184475, 'fraction_numerical': 0.005704578875310583, 'mean_word_length': 4.263277288497465, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 32, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Extending Coinductive Logic Programming with Co-Facts

We introduce a generalized logic programming paradigm where programs, consisting of facts and rules with the usual syntax, can be enriched by co-facts, which syntactically resemble facts but have a special meaning. As in coinductive logic programming, interpretations are subsets of the complete Herbrand basis, including infinite terms. However, the intended meaning (declarative semantics) of a program is a fixed point which is not necessarily the least, nor the greatest one, but is determined by co-facts. In this way, it is possible to express predicates on non well-founded structures, such as infinite lists and graphs, for which the coinductive interpretation would be not precise enough. Moreover, this paradigm nicely subsumes standard (inductive) and coinductive logic programming, since both can be expressed by a particular choice of co-facts, hence inductive and coinductive predicates can coexist in the same program. We illustrate the paradigm by examples, and provide declarative and operational semantics, proving the correctness of the latter. Finally, we describe a prototype meta-interpreter.


Introduction
Coinductive logic programming [11,13,12,4] extends standard logic programming with the ability of reasoning about infinite objects and their properties. Whereas syntax of logic programs remains the same, semantics is different. To illustrate this, let us consider the following logic program which defines some predicates on lists of integers, constructed with the standard function symbols [] of arity 0 for the empty list and [ | ] of arity 2 for the list consisting of a head element and a tail. For simplicity, we will consider built-in integers, as they are in Prolog. The expected meaning is that all_pos(l) holds if all the elements of l are positive, member(x,l) if x is an element of l, max(l,n) if n is the greatest element of list l. As will be illustrated in detail in Sect. 2, in standard logic programming terms are inductively defined, that is, are finite, and predicates are inductively defined as well. In the example program, only finite lists are considered, such as, e.g., [1|[2|[]]], and the three predicates are correctly defined on such lists.
In coinductive logic programming, instead, terms are coinductively defined, that is, can be infinite, and predicates are coinductively defined as well. In the example program, also infinite lists such as [1|[2|[3|[4|...]]]], are considered, and the coinductive interpretation of the predicate all_pos gives the expected meaning on such lists. However, this is not the case for the other two predicates: for member the correct interpretation is the inductive one, whereas for max neither the inductive nor the coinductive interpretation are correct: with the former the predicate is always false on infinite lists, with the latter max(l,n) is true whenever n is greater than all the elements of l.
The last example shows that the coinductive interpretation of predicates is sometimes not precise enough, in the sense that also wrong facts are included. This problem can be found, and has been studied, also in other programming paradigms, and some solutions have been proposed which allow the programmer to interpret corecursive definitions not in the standard coinductive way [8,9,2,5,6].
In this paper, we solve the problem in a more foundational way, by applying to the case of logic programs a notion recently introduced in the more general framework of inference systems [3] (indeed, a logic program can be seen as an inference system where judgments are atoms). That is, programs, consisting of facts and rules with the usual syntax, can be enriched by co-facts (corresponding to coaxioms in [3]), which syntactically resemble facts but have a special meaning: intuitively, they can only be applied "at infinite depth" in a proof tree, as will be formally defined in the following. By adding co-facts, the intended meaning (declarative semantics) of a program can be a fixed point which is not necessarily the least, nor the greatest one.
In this way, it is possible to express predicates on non well-founded structures, such as infinite lists and graphs, for which the coinductive interpretation would be not precise enough. Moreover, this paradigm nicely subsumes standard (inductive) and coinductive logic programming, since both can be expressed by a particular choice of co-facts, hence inductive and coinductive predicates can coexist in the same program.
For what concerns operational semantics, in coinductive logic programming standard SLD resolution is replaced by co-SLD resolution [13,4], which, roughly speaking, keeps trace of the already encountered goals, called (dynamic) coinductive hypotheses, so that, when a goal is encountered the second time, it is considered successful. In this paper, we define an operational semantics of logic programs which is similar to co-SLD resolution, but takes co-facts into account, and prove its correctness with respect to the proposed declarative semantics. The proof is interesting since it is a non-trivial application of the bounded coinduction principle introduced in [3].
The operational semantics we define is in big-step style, as also proposed for co-SLD resolution [4], and, hence, is amenable for directly deriving an implementation; indeed, we have implemented in SWI-Prolog a prototype meta-interpreter, whose clauses are driven by our operational semantics, and with which we have been able to successfully test all examples shown in this paper, and many others.
The rest of the paper is organized as follows: in Sect. 2 we introduce logic programs with co-facts, their declarative semantics, and the bounded coinduction principle to reason on such programs, illustrating the notions with some examples. In Sect. 3 we formally define operational semantics, show a derivation example, and prove soundness with respect to declarative semantics. In Sect. 4 we describe the prototype meta-interpreter. In Sect. 5 we summarize our contribution, survey related work, and discuss further work.
Assume a signature consisting of sets of predicate symbols p, function symbols f , and variable symbols X , each one with an associated arity ≥ 0, being 0 for variable symbols. A function of arity 0 is called a constant.
Terms are (possibly infinite) trees where nodes are labeled with function and variable symbols and the number of children of a node corresponds to the symbol arity (for a more formal definition based on paths see, e.g., [4]). Atoms are (possibly infinite) trees where the root is labeled with a predicate symbol and other nodes are labeled with function and variable symbols, also accordingly with the arity. Terms and atoms are ground if they do not contain variable symbols, finite (or syntactic) if they are finite trees. A logic program P is a set of (definite) clauses of shape A :− B 1 , . . . , B n , where A, B 1 , . . . , B n are finite atoms. A clause where n = 0 is called a fact, otherwise it is called a rule.
A substitution θ is a mapping from a finite subset of variables into terms. We write tθ for the application of a substitution θ to a term t. We call tθ an instance of t. These notions can be analogously defined on atoms and clauses. A substitution is ground (or grounding) if it maps variables into ground terms, it is syntactic if it maps variables into finite (syntactic) terms. The declarative semantics of a logic program describes its meaning in an abstract way, as the set of ground atoms which are defined to be true by the program, in a sense to be made precise depending on the kind of declarative semantics we choose. In the following paragraphs, we briefly recall the standard declarative semantics of logic programs, then their coinductive declarative semantics, and finally we define the declarative semantics generated by co-facts and discuss its advantages.
Standard declarative semantics In the standard declarative semantics of logic programs, only finite terms and atoms are considered. The Herbrand universe HU is defined as the set of finite ground terms, and the Herbrand base HB as the set of finite ground atoms. Sets I ⊆ HB are called interpretations. Given a logic program P, the (one step) inference operator T P : ℘(HB) → ℘(HB) is defined as follows: where ground(P) is the set of instances of clauses in P obtained by a ground syntactic substitution.
An interpretation is a model of a program P (is closed with respect to P) if T P (I) ⊆ I. The standard declarative semantics of P is the least interpretation which is a model taking as order set inclusion, that is, the intersection of all closed interpretations. Defining a proof tree for a ground atom A as a tree where the root is A, nodes are ground instances of rules, and leaves are ground instances of facts, the standard declarative semantics can be equivalently characterized as the set of finite ground atoms which have a finite proof tree.
It is easy to see that, with this definition, the predicates of the example program introduced in Sect. 1 have the expected meaning on finite lists. For instance, for the predicate max we obtain all atoms max(l,n) where l is a (ground term representing a) finite list and n is the greatest element of l.
Co-inductive declarative semantics A limit of the standard declarative semantics described above is that we cannot define predicates on non-well-founded structures, such as infinite lists or graphs. Considering our running example, we would like to define the predicates all_pos, member, and max on infinite lists as well. To obtain this, first of all infinite terms and atoms should be included. The complete Herbrand Universe co-HU [10] is the set of (finite and infinite) ground terms. The complete Herbrand base co-HB is the set of (finite and infinite) ground atoms. Sets I ⊆ co-HB are called co-interpretations.
We can define the (one step) inference operator T P : ℘(co-HB) → ℘(co-HB) analogously to that above: where co-ground(P) is the set of instances of clauses in P obtained by a ground substitution. 1 Again as above, a co-interpretation is a model of a program P (is closed with respect to P) if T P (I) ⊆ I, and we can consider the the least co-interpretation which is a model, that is, the intersection of all closed co-interpretations. This co-interpretation, called in the following inductive (declarative) semantics of P and denoted Ind(P), generalizes the standard declarative semantics of predicates to infinite terms. However, in order to prove predicates on such infinite terms, we would like to allow infinite proof trees as well, and to this end a different declarative semantics can be adopted, explained below.
A co-interpretation I is a co-model of P (is consistent with respect to P) if and only if I ⊆ T P (I). The coinductive (declarative) semantics of P, denoted CoInd(P), is the greatest co-interpretation which is a co-model taking as order set inclusion, that is, the union of all consistent co-interpretations. Equivalently, CoInd(P) can be characterized as the set of ground atoms which have a (finite or infinite) proof tree.
Let us analyze what happens in the running example. Consider first the predicate all_pos. It is easy to see that, with the inductive semantics Ind(P), this predicate has the expected meaning only on finite lists (as in the standard semantics) and on infinite lists which have a non positive element. However, for l term representing an infinite list of positives, e.g., l = Hence, this predicate is a typical example where coinductive semantics is necessary (when including infinite terms), and provides the expected meaning. However, this is not the case for the other two predicates. More precisely, for l (term representing an) infinite list: • member(x,l) always holds. In this case, the coinductive semantics CoInd(P) seems not to be the right choice, and the desired semantics is obtained by taking the inductive semantics (least model) on infinite lists as well, that is, Ind(P). For this reason, in coinductive logic programming the programmer can specify by a special notation that some predicates should be interpreted inductively rather than coinductively. • max(l,n) holds whenever n is greater than all the elements of l. In this case, the coinductive semantics includes the desired semantics (and it is necessary for this, since max(l,n) would never hold in the inductive semantics), but it is not precise enough. Declarative semantics generated by co-facts In order to define this semantics, first of all the syntax is slightly generalized allowing, besides facts and rules, co-facts, written .A. Co-facts are finite atoms, hence syntactically resemble facts, but have a special meaning. Below is the version equipped with co-facts of the running example. In the following, the metavariable C denotes a set of co-facts (finite atoms). The (declarative) semantics of a program P generated by co-facts C, denoted Gen(P, C), is defined as follows.
• First, we consider the program P ⊔C obtained by enriching P by the co-facts in C considered as facts, and we take its inductive semantics Ind(P ⊔C ). • Then, we take the largest co-model which is included in Ind(P ⊔C ). In other words, we take the coinductive interpretation of P where, however, clauses are instantiated only on elements of Ind(P ⊔C ). Note that Gen(P, C) is different from CoInd(P) ∩ Ind(P ⊔C ). For instance, let P be the program (1) and C be the singleton set consisting of the co-fact .( p (0)) Then, CoInd(P) = {p(0), p(1)}, and Ind(P ⊔C ) = {p(0)}. Hence the intersection is {p(0)}, whereas Gen(P, C) = / 0. As we have shown in [3] in the more general framework of inference systems, Gen(P, C) corresponds to a fixed-point of the operator T P which is neither the greatest, nor the least one.
In terms of proof trees, Gen(P, C) is the set of ground atoms which have a (finite or infinite) proof tree in P whose nodes all have a finite proof tree in P ⊔C . Taking this semantics, all the predicates in the running example get the expected meaning. Indeed, for l (term representing an) infinite list: • all_pos(l) holds for l infinite list of positives, since the atom all_pos(l) has the previously shown infinite proof tree, and all its nodes have a (trivial) finite proof tree in P ⊔C , consisting in an instantiation of the co-fact. • member(x,l) only holds if x belongs to l. Otherwise, there would exist an infinite proof tree in P, but its nodes have no finite proof tree in P ⊔C , since there are no co-facts, and the only fact is not applicable. • max(l,n) only holds when n is the greatest element of l. In this case, as shown at page 4, there exists an infinite proof tree in P whenever n is greater than all the elements of l. However, a finite proof tree in P ⊔C for each node only exists when n belongs to the list, hence is actually the greatest element. For instance, the two nodes of the infinite proof tree ( whereas there is no finite proof tree for the nodes of the infinite proof tree (T2). In other words, co-facts allow the programmer to "filter out" atoms which should not be true, making the semantics precise. Note that the condition to have a finite proof tree in P ⊔C trivially holds for nodes which are roots of a finite subtree (a finite proof tree in P is a finite proof tree in P ⊔C as well), hence is only significant for nodes which occur in an infinite path. Moreover, if the infinite tree is rational, that is, has a finite number of different subtrees, then an infinite path always consists of (possibly) a finite prefix and a period. Hence, if the condition holds for the first node of the period, then it holds for all the other nodes. In the example of (T1) above, another finite proof tree for the second node max([2|[1|[2|...]]],2) can be obtained from (FT1) for the first node: Correspondingly, in the operational semantics which will be provided in Sect. 3, standard SLD resolution in P ⊔C is triggered when an atom is encountered the second time.
Note also that, as the examples above clearly show, the inductive and coinductive semantics can be obtained as special cases of the semantics generated by co-facts of a program, notably: • the inductive semantics when the set of co-facts is empty; • the coinductive semantics when the set of (ground instances of) co-facts is co-HB.
That is, co-facts allow to mix together, without any need of a special notation, predicates for which the appropriate interpretation is either inductive or coinductive, and to express predicates for which the appropriate interpretation is neither of the two, as the max example shows.
Let G be a set of ground atoms, corresponding to the intended meaning of some predicates.
In order to prove that the the atoms in G are defined to be true by a program P enriched by cofacts C, that is, G ⊆ Gen(P, C), we can use the following bounded coinduction principle, which is a generalization of the standard coinduction principle. This and other proof techniques are illustrated in the more general framework of inference systems in [3]. Boundedness G ⊆ Ind(P ⊔C ), that is, each atom in G has a finite proof tree in P ⊔C Consistency G ⊆ T P (G), that is, for each atom A ∈ G, A :− B 1 , . . . , B n ∈ co-ground(P) for some B 1 , . . . , B n ∈ G then G ⊆ Gen(P, C).
Proof. The two conditions corresponds to require that G is a co-model of P (is consistent with respect to P) which is bounded by (included in) Ind(P ⊔C ), and Gen(P, C) is defined as the largest such comodel.
The standard coinduction principle can be obtained as a specific instance of the principle above, when (ground instances of) C coincide with co-HB; for this particular case the first condition trivially holds.
We illustrate the proof technique by formally proving that, in the running example, we can derive all atoms in the set G max = {max(n, l) | n greatest element of l}.
• To prove boundedness, we have to show that, for each max(l,n) such that n is the greatest element of l, max(l,n) has a finite proof tree in P ⊔C . This can be easily shown. • To prove consistency, we have to show that, for each max(l,n) such that n greatest element of l, max(l,n) is the consequence of (an instance of) a clause with all atoms of the body in G max . This can be easily shown, indeed, if n is the greatest element of l, then l = [n ′ |l ′ ] with n ′ ≤ n and n greatest element of l ′ . Hence, max(l,n) is the consequence of the following instance of the rule: The same proof technique will be used in the next section to show that the operational semantics is sound with respect to the semantics generated by co-facts.

Big-step operational semantics
In this section we define an operational counterpart of the semantics generated by co-facts introduced in Sect. 2, and prove its correctness.
This operational semantics is a generalization of SLD [10,7] and co-SLD [11,13,12] resolution. However, it is presented, rather than in the traditional small-step style, in big-step style, as introduced in [4]. This style turns out to be simpler since coinductive hypotheses (see below) can be kept local. Moreover, it naturally leads to an interpreter, and the proof of soundness with respect to declarative semantics is more direct since we compare two inference systems. For a proof of equivalence of big-step and small-step co-SLD resolution see [4].
We introduce some notations. First of all, in this section the metavariable A denotes finite (syntactic) atoms and the metavariables s,t denote finite (syntactic) terms. An equation has shape s = t where s and t are finite terms. We write E for a set of equations. Equations allow a finite (syntactic) representation also of rational terms and atoms, that is, having a finite number of different subterms, see, e.g., [1,4] for the details. Finally, a goal is a sequence of atoms, and the metavariable G denotes a syntactic goal, that is, a sequence of finite atoms. The empty sequence is denoted by ε.
The operational semantics is defined by a judgment ⊢ P,C G ⇒ E, meaning that, given a program P and a set of co-facts C, resolution of the (syntactic) goal G succeeds and produces a set of equations E that describes a solution of the goal. For instance, assuming P and C from the previous section, which define, among others, the predicate max computing the greatest element of a list, it would be possible to derive the following judgment This judgment is defined following a schema which is similar to co-SLD resolution, in the sense that resolution keeps track of the already encountered atoms, which are called (dynamic) coinductive hypotheses [13]. However, when the same atom A is encountered the second time, rather than just considering A successful as it happens in co-SLD resolution, standard SLD resolution of A is triggered in the program P ⊔C obtained by enriching P by the co-facts in C.
Formally, two auxiliary judgments are introduced: • S ⊢ P,C G E ⇒ E ′ , meaning that, given a program P and a set of co-facts C, resolution of the goal represented by G and E, under the coinductive hypotheses S, succeeds producing a set of equations E ′ which describes a solution of the goal.
(empty) ⊢ P ε E ⇒ E (step) p(t 1 , . . . ,t n ) :− A 1 , . . . , A m renaming of a clause in P with fresh variables . . , A m renaming of a clause in P with fresh variables Rules (inductively) defining these judgments are shown in Fig. 1. The first two rules define the judgment ⊢ P G E ⇒ E ′ corresponding to standard SLD resolution. In rule (empty), resolution of the empty goal succeeds. In rule (step), an atom p(s 1 , . . . , s n ) is selected from the goal to be resolved, and a clause of the program is chosen such that the selected atom unifies with the head of the clause, as expressed by the fact that adding the equations s 1 = t 1 , . . . , s n = t n to the current set we get a solvable set of equations. Then, resolution of the original goal succeeds if resolution of both the body of the clause and the remaining goal succeed.
The following three rules define the judgment S ⊢ P,C G E ⇒ E ′ corresponding to an intermediate step of resolution. Rules (co-empty) and (co-step) are analogous to rules (empty) and (step). The only difference is that, in rule (co-step), in the resolution of the body of the clause, the selected atom is added to the current set of coinductive hypotheses. In this way, rule (co-hyp) can handle the case when resolution encounters the same atom for the second time, that is, more formally, the selected atom unifies with a coinductive hypothesis, as expressed by the fact that adding the equations s 1 = t 1 , . . . , s n = t n to the current set we get a solvable set of equations. In this case, standard SLD resolution of such atom is triggered in the program P ⊔C obtained by enriching P by the co-facts in C, and resolution of the original goal succeeds if both such standard SLD resolution of the selected atom and resolution of the remaining goal succeed.
Finally, rule (main) defines the main judgment ⊢ P,C G ⇒ E corresponding to an initial step of resolution, where the goal is syntactic, that is, no equation has been produced yet.
In the following, to avoid confusion with proof trees considered in Sect. 2, trees obtained by instantiating the rules of big-step operational semantics are called derivations.
A derivation example Assuming P and C from the previous section, which define, among others, the predicate max computing the greatest element of a list, we show a derivation for the judgment For keeping the derivation simpler, in rules (co-step) and (step) we do not manifest some substitutions, but, instead, we implicitly apply them in the resulting goals. Furthermore, we consider the predicate _ is max(_,_) to be predefined, as it is the case in real Prolog systems; for it we have introduced a special semantic rule (labeled with p, for predefined) that deals with standard inductive predefined predicates (see Sect. 4). Finally, for space reasons we have abbreviated the names of the applied rules.
In the whole derivation the co-fact for max is used just once in rule (step) marked with (s*) in ∇ 1 derivation; the co-fact could be employed also in rule (step) in derivation ∇ 1 , but without success, since the substitution {M2=M,M2=1} cannot satisfy the goal M1 is max(2,M2),M is max(1,M1).

Soundness proof
The big-step operational semantics is sound with respect to the declarative semantics defined in Sect. 2. That is, if resolution of the goal G succeeds producing a set of equations E which describe a solution of the goal, then (any ground instance of) this solution is a set of atoms which are true in the declarative semantics. Formally, set gsol(E) = {θ | θ ground, tθ = t ′ θ for all t = t ′ ∈ E} the set of the ground solutions of E, necessarily defined on the set V(E) of the variables occurring in E. In the following, when we pick a substitution from gsol(E), we will implicitly assume that this substitution has V(E) as domain. Note that the set of ground solutions is antitone with respect to set inclusion, that is, if E 1 ⊆ E 2 then gsol(E 2 ) ⊆ gsol(E 1 ). Soundness can be stated as follows.

Theorem 3.1 (Soundness). If ⊢ P,C G ⇒ E holds then, for each θ ∈ gsol(E), Gθ ⊆ Gen(P, C).
The proof of soundness is an application of the bounded coinduction principle (Theorem 2.1) introduced in Sect. 2. For sake of clarity, we provide the proof in a top-down manner, that is, we first give the proof schema, and then state and prove the three needed subtheorems.
Proof of Theorem 3.1. Thanks to Lemma 3.2(4), the statement can be equivalently formulated as OpSem(P, C) ⊆ Gen(P, C). By bounded coinduction, we have to show that: Boundedness OpSem(P, C) ⊆ Ind(P ⊔C ), that is, each A ∈ OpSem(P, C) has a finite proof tree in P ⊔C .
The two conditions can be proved as follows.
• To prove boundedness, we have to show that, if ⊢ P,C A ⇒ E, θ ∈ gsol(E), then Aθ ∈ Ind(P ⊔C ). This can be proved by two steps: • Consistency can be proved as follows: -⊢ P,C A ⇒ E implies that there exist B 1 , . . . , B n such that Aθ :− B 1 θ , . . . , B n θ ∈ co-ground(P) and ⊢ P,C B 1 , . . . , B n ⇒ E ′ with E|E ′ (by Theorem 3.4) , that follows from the following facts: Now we detail the proof, by stating and proving the three theorems and the lemma used above. Some proofs are given in Appendix A. We first introduce the following notations. If A = p(t 1 , . . . ,t n ), and B = p(s 1 , . . . , s n ), then we write E A=B for the set of equations that represents the unification of A with B, that is, E A=B = {s 1 = t 1 , . . . , s n = t n }.
The boundedness condition is obtained by Theorem 3.2 and Theorem 3.3. The former states that resolution under coinductive hypotheses implies standard SLD resolution in the program enriched by co-facts, the latter states that standard SLD resolution is sound with respect to the inductive semantics.
We start with an auxiliary lemma.
Proof. Straightforward induction on inference rules.
The following theorem states that if resolution under coinductive hypotheses of a goal succeeds, then standard SLD resolution of the goal in the program enriched by co-facts succeeds as well.
Proof. By induction on the inference rules which define S ⊢ P,C G E 1 ⇒ E 2 .
(co-step) By inductive hypothesis we get that . . , A n a fresh renaming of a clause in P ⊔C . By , thus by rule (step) we get the thesis.
(co-hyp) By hypothesis and by Lemma 3.1(1) we get that . . , A n a fresh renaming of a clause in P ⊔C . By inductive hypothesis we get . Therefore by rule (step) we get the thesis.
The following theorem states that if standard SLD resolution of a goal succeeds, producing a set of equations E which describes a solution of the goal, then this solution is a set of atoms which are true in the inductive semantics. In other words, this theorem states the standard soundness property of SLD resolution. The theorem could be derived by showing equivalence of the ⊢ P A / 0 ⇒ E judgment with the traditional small-step definition of SLD resolution (as done in [4] for co-SLD resolution), and relying on the well-know soundness of the latter. A direct proof can be done by induction on the rules which define ⊢ P A / 0 ⇒ E, as stated below Theorem 3.3 (Soundness of standard SLD resolution). If ⊢ P A / 0 ⇒ E then, for each θ ∈ gsol(E), Aθ ∈ Ind(P).
We state now some lemmas needed to prove Theorem 3.4. The following lemma states some properties of the judgment S ⊢ P,C G E ⇒ E ′ . In particular, points 1 and 2 state a form of monotonicity with respect to the set of coinductive hypotheses and the set of input equations: that is, we can freely add coinductive hypotheses and remove input equations preserving the results of the evaluation. Point 3 states another monotonicity property: we can add input equations provided that this addition does not break the solvability of the output system of equations. Finally, point 4 states a decomposition property: the evaluation of a single atom in a goal produces a subset of the equations produced by the entire goal.
Lemma 3.2. If S ⊢ P,C G E 1 ⇒ E 2 holds, then: Proof. Straightforward induction on inference rules.
As a consequence we get the following result.
Proof. From point 2 and 3 of Lemma 3.2.
The proof can be found in the Appendix.
Proof. Since by hypothesis ⊢ P,C A ⇒ E holds, we have necessarily applied rule (main), hence / 0 ⊢ P,C A / 0 ⇒ E holds. We have also necessarily applied rule (co-step), hence {A} ⊢ P,C B 1 , . . . , B n E A=A ′ ⇒ E holds, for some fresh renamed clause A ′ :− B 1 , . . . , B n in P such that E A=A ′ is solvable. Therefore for all θ ∈ gsol(E) we have A ′ θ :− B 1 θ , . . . , B n θ ∈ co-ground(P), and since E A=A ′ ⊆ E, that implies Aθ = A ′ θ , we get Aθ :− B 1 θ , . . . , B n θ ∈ co-ground(P). Now we have to show that / 0 ⊢ P,C B 1 , . . . , B n / 0 ⇒ E ′ holds for some E ′ such that E|E ′ . We prove this statement in two steps.
1. First we prove that / 0 ⊢ P,C B 1 , . . . , B n E A=A ′ ⇒ E ′′ for some E ′′ with E|E ′′ 2. Then we remove the equations in E A=A ′ .
(co-hyp) We consider the case where the rule has the following shape, if B unifies with an atom in S the thesis follows from inductive hypothesis by applying rule (co-hyp). (co-hyp) By hypothesis {A} ⊢ P,C B 1 , . . . , B n E A=A ′ ⇒ E holds with A ′ :− B 1 , . . . , B n a fresh renaming of a clause in P. Let ρ be a renaming of variables in V(E) which maps variables in V(A) in themselves, and other variables to fresh variables, then {A} ⊢ P,C B ′ 1 , . . . , B ′ n E A=A ′ ρ ⇒ Eρ holds with B ′ i = B i ρ and θ ∈ gsol(E) iff ρ −1 θ ∈ gsol(Eρ) and θ |ρ −1 θ . Now we have to show that Eρ ∪ E 1 ∪ E B=A ′ ρ is solvable; to this aim we consider a substitution θ ∈ gsol(E), and note that, since E 1 ⊆ E, gsol(E) ⊆ gsol(E 1 ), this implies θ ∈ gsol(E 1 ), therefore by Lemma 3.4, . Thus by Lemma 3.2(1), Corollary 3.2 and Lemma 3.

Implementation
We have implemented a prototype meta-interpreter in SWI-Prolog, driven by the rules of the big-step operational semantics defined in Sect. 3; the complete source code can be found in Appendix B, and it is publicly available on the Web 3 together with a unit test-suite.
Tests include the predicates on lists considered in the examples provided in Sect. 2, but also other predicates on lists, as well as predicates defined on repeating decimals, grammars, graphs, and infinite regular trees [3].
The three main predicates solve/1, solve_gfp/2, and solve_lfp/2 implement the semantic judgments ⊢ P,C G ⇒ E, S ⊢ P,C G E ⇒ E ′ , and ⊢ P G E ⇒ E ′ , respectively. As usual, sets of equations do not need to be explicitly manipulated by the meta-interpreter, which relies on the built-in unification mechanism offered by the Prolog interpreter, therefore the above mentioned predicates take less arguments than their corresponding judgments. Despite this fact, solve_gfp, and solve_lfp have the same arity, because solve_lfp needs an extra argument (in comparison to ⊢ P G E ⇒ E ′ ) to guarantee termination for some queries (see more explanations below).
Differently from the operational semantics, the meta-interpreter is fully deterministic and follows the standard selection rules for goal atoms (leftmost) and clauses (topmost/leftmost, as supported by the system predicate clause).
Despite the meta-interpreter is driven by the semantic rules, there is no one-to-one correspondence between the rules and the meta-interpreter clauses, for several reasons explained below.
The meta-interpreter allows a correct management of predefined predicates which can be identified thanks to the SWI-Prolog system predicates; for instance, the examples shown in Sect. 2 uses the built-in predicates >, \=, and max. To handle such predicates, we have added a specific clause which does not have a counterpart in the operational semantics: if an atom uses a predefined and necessarily inductive (either built-in, or defined in the standard library) predicate, then the meta-interpreter delegates its resolution to the Prolog interpreter.
Since the meta-programming facilities manage goals as non-empty sequences of atoms (the empty goal is represented by the single atom true), there are no clauses corresponding to the semantic rules (empty) and (co-empty); rather, there are two clauses (named seq and co-seq) which simply decompose nonsingleton goals in their leftmost atom and rest of atoms, while the clauses dealing with singleton goals correspond to (step), (co-step), and (co-hyp) rules, with the difference that in their bodies there is no atom for resolving the remaining goal, as happens for the corresponding judgment with G 1 , G 2 .
From the complexity results concerning coinductive programming [4] we know that determining whether a goal succeeds w.r.t. the coinductive semantics is not even semi-decidable, and, hence, the same applies also to our extension with co-facts which includes the standard coinductive semantics.
The interpreter limits non termination in two ways: • a cut is inserted right after atom co_find(Atom, AtomList) in the body of the clause for solve_gfp corresponding to rule (co-hyp); in this way, the clause corresponding to (co-step) is never applied for an atom which unifies with an element in the list AtomList of the coinductive hypotheses (that is, rule (co-hyp) is applicable); this ensures that non termination is avoided when a "loop" in the proof tree is detected. Of course, with the insertion of such a cut we may miss some correct answer [2].
• we have inserted an additional clause (called cut) for the solve_lfp predicate which uses an association to map encountered atoms (modulo unification) to the number of times they have been already processed by the meta-interpreter; clause step updates such an association, by checking whether the currently processed atom unifies with an atom already present in the association; since solve_lfp has to build a finite proof tree, no substitution is applied when unification succeeds. Clause cut, which precedes clause step, fails with no backtracking if, according to the association, the current atom has been already processed twice. Also in this case, we ensure termination at the cost of missing some correct answer.
Clause cut is also responsible for co-facts: it attempts to apply co-facts only when the corresponding atom is found in the association (but only for the first time); in this way termination is guaranteed in more cases. Since co-facts are managed as facts with the system predicate clause, it has been pretty easy to extend the meta-interpreter to take into account also the possibility of defining co-clauses (see further comments in Sect. 5).

Conclusion
We have proposed a generalized logic programming paradigm inspired by the notion of inference system with coaxioms [3], where it is possible to consider interpretations which are between the inductive and the coinductive one. At the model-theoretic level (declarative semantics) this has been achieved by taking as semantics of a program the largest co-model of the program included in the least model of the program enriched by co-facts; at the operational level we have defined a big-step operational semantics which is a refinement of co-SLD resolution: when the same goal is encountered the second time, its standard SLD resolution is triggered in the program enriched by co-facts.
We have proved that such an operational semantics is sound with respect to the declarative semantics; furthermore, the big-step semantics rules have driven the implementation of a prototype meta-interpreter that has allowed us to successfully experiment our generalized logic programming paradigm.
Coinductive logic programming has been initially investigated and implemented by Simon et al. [13,12]; since the earlier stages, the problem has been recognized that not all predicate definitions require a coinductive interpretation; for instance, Simon et al. have pointed out this issue for the member predicate, whose semantics is inductive even when infinite lists are considered. Anyway, to our knowledge, no current implementation of coinductive logic programming supports the extension of inductive predicates for the complete Herbrand base, neither the ability of defining programs where coinductive and inductive predicates can be freely mixed together.
Similar issues have been investigated in the context of coinductive functional [8,9], and objectoriented [5,6] paradigms, but the proposed solutions lack proof principles useful for proving correctness of programs written in these extended paradigms.
We have commented in Sect. 4 that the prototype meta-interpreter naturally supports not only cofacts, but also co-clauses, and the big-step semantics can be trivially extended to take into account this possibility, but it would be interesting to investigate whether this generalization has a natural counterpart at the level of the declarative semantics.
For what concerns the implementation, much more work is required to guarantee that the extension of logic programming with co-facts can be effectively used in practice. The meta-interpreter offers a simple solution to rapid prototyping of an implementation of the operational semantics by exploiting the reflection facilities of Prolog, but is far from being an efficient solution. Furthermore, the combination of the two predicates solve_gfp and solve_lfp for coinductive and inductive reasoning, respectively, has a bad impact on the performance because in fact a proof tree needs to be built twice. It would be interesting to investigate more clever algorithms to avoid such a duplication, or, at least, identify conditions on logic programs which are sufficient to guarantee more efficient implementations.
Another direction for further work consists in studying restricted classes of logic programs for which the operational semantics of co-facts presented here turns out to be sound and complete.
Suppose that B unifies with A, that is E 1 ∪ E B=A is solvable. By hypothesis E 3 ∪ E A=A ′ is solvable, thus by inductive hypothesis we get S ⊢ P,C G 1 , G 2 E 2 ⇒ E ′ 3 with gsol(E 3 ∪ E A=A ′ ) ⊆ gsol(E ′ 3 ). Since E 2 ⊆ E 3 we know that gsol(E 3 ∪ E A=A ′ ) ⊆ gsol(E 2 ∪ E A=A ′ ); moreover since E B=A ⊆ E 2 , we get that gsol(E 2 ∪ E A=A ′ ∪U ni f yEqBA ′ ) = gsol(E 2 ∪ E A=A ′ ), thus, by Corollary 3.1, we get that . Hence by Corollary 3.2 we get that S ∪ {A ′ } ⊢ P,C G 1 , . Finally we get the thesis by applying rule (co-hyp).