There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational specification language called [CafeOBJ][1] (see [introduction][2]). In particular, the [BOOL module][3] can be viewed as a formalisation of propositional logic defined by a set of equations. My basic idea is to transform First Order Predicate Logic sentences (FOPL) into [order-sorted][4] equations consisting of [Boolean valued functions][5] (BVF). Then in proofs the BVF are instantiated with constants and [proofs][6] are executed using term rewriting. See [related question][7]. Below, I present my proposed formalisation, proof, and an example. 

**Formalisation**

 FOPL sentences are transformed to equational form as follows.
 - Predicates are converted to BVFs.
 - All variables are assumed to be universally quantified. 
 - Skolem constants and functions are used to represent existential quantified variables. 
 - The translated sentences are written on the right hand side of equations.
 - The left side of the equations is a named BVF whose arguments are the variables necessary for the right hand side translated sentence.

For example the FOPL sentence

 $\forall x  (\forall y  (Animal(y)  \implies Loves(x,y)) \implies (\exists z  Loves(z,x)))$

Would be translated in the following order-sorted CafeOBJ equation:

    eq s1(x:Person,y:Animal)  = loves(x,y) implies loves(G(x),x)  .

The variables are each given a sort or type. Note, the Skolem function $G(x)$ has only one argument because the $y$ in the antecedent is not in scope in the consequent. The general form of which is $LeftEqName_1(Args)=Expression_{BVF}$. Because we have sorts (or types) in CafeOBJ, we do not need the predicate $Animal(y)$.



**Proof**

A combination of Equational Logic, Boolean Algebra, and order sorted term rewriting is used for proof. The general form of the proof is:

$(LeftEqName_1(InstantiatedArgs) \land LeftEqName_2(InstantiatedArgs) \land \dots \land LeftEqName_n(InstantiatedArgs)) \implies BVF$ .

This is intended to represents an implication whose antecedent is the conjunction of the original FOPL sentences. Universal quantified variables in the original equations are replaced by fresh constants in the proofs.Universal quantified variables can also be instantiated by constants from the original set of FOPL sentences. The [Theorem of Constants][8] states that universal variables in the original equations can be replaced by fresh constants in a proof. 

I use CafeOBJ's term rewriting command called [reduce][9] , which  recursively matches each term with the appropriate left-hand side of an equation and replaces it with the right-hand side, CafeOBJ reduces a logical formula into an exclusive-or normal.  A term of Bool reduces to an exclusive disjunction of conjunction. It is known that the exclusive-or normal form is true if the input term is valid, and false if it is unsatisfiable.
 
 **Example**

Below is a CafeOBJ  order sorted example of the proposed method. In this case no universals are needed in the proof, we only need constants from the original FOPL sentences. I also include a single-sorted FOPL version.

 

       mod* CURIOSITY-EQL-OSA {
        [Cat < Animal Person < Thing ]
        pred    kills  : Person Animal
        pred   loves : Thing Thing
        op tuna  : -> Cat 
        ops jack  curiosity : -> Person
          
        preds  s3 s6 : Thing
        preds s4 s5 :
        pred s1   : Person  Animal
        pred s2   : Person  Person 
        op G : Person   -> Person
        op F : Person   -> Animal
        -- Everyone who loves all animals is loved by someone.
        eq s1(x:Person,y:Animal)  = loves(x,y) implies loves(G(x),x)  .
        -- Anyone who kills an animal is loved by no one.					   
        eq s2(x:Person,y:Person)  =    kills(x,F(x)) implies (not (loves(y,x))) .					   
        -- Jack loves all animals.
        eq s3(x:Animal) = loves(jack,x)  . 
       -- Either jack or curiosity killed tuna the cat
        eq s4 =   kills(curiosity,tuna) or kills(jack,tuna) .
        }
        
        open CURIOSITY-EQL-OSA .
        --> Show that jack did not kill any animal
        red (s1(jack,F(jack)) and s2(jack,G(jack))  and s3(F(jack))) implies (not (kills(jack,F(jack)) )) .
        --> Use existential generalization (existential introduction).
        let s4a =   kills(curiosity,tuna) or kills(jack,F(jack)) .
        red ((not kills(jack,F(jack))) and s4a) implies kills(curiosity,tuna) .
        --> Gives true
        close
        -- Alternatively
        open CURIOSITY-EQL-OSA .
        eq F(jack) = tuna . -- assume tuna is the animal jack kills (a contradiction).
        red (s1(jack,tuna) and s2(jack,G(jack)) and s4 and s3(tuna)) implies (kills(curiosity,tuna) ) .
        --> Gives true
        close


**Single sorted first order formalisation and proof**


[![First Order Formalisation and proof][10]][10]

The FOPL proof uses natural deduction. Lines 1-6 are axioms which are assumed to be true. The justification for each proof step are listed on the right. The text ‘FO Con’ means first order consequence, which uses well known FOL proof techniques e.g. Line 16 is justified by disjunctive syllogism from lines 4 and 15.
 
  
 


  [1]: https://cafeobj.org/
  [2]: https://cafeobj.org/intro/en/
  [3]: https://equational.wordpress.com/#bool-module
  [4]: https://cafeobj.org/intro/en/sorts.html
  [5]: https://ncatlab.org/nlab/show/boolean-valued+function
  [6]: https://cafeobj.org/intro/en/proofscores.html
  [7]: https://cs.stackexchange.com/questions/119985/proving-a-first-order-logic-theorem-in-equational-logic-with-a-term-rewriting-sy
  [8]: https://equational.wordpress.com/2016/09/07/algebraic-specification/#theorem-of-constants
  [9]: https://cafeobj.org/intro/en/reduction.html
  [10]: https://i.sstatic.net/hfw63.png