Simply put, yes. And if computers are used from the vantage of cognitive scientists understanding human thought, it is called it experimental philosophy (SEP).
If you've followed some of my posts, you'll know I blather on about how logic is grounded in psychology, and the Fregean logicist program was a useful detour in the same way miasma theory lead to the death of countless pregnant women when Ignaz Semmelweis had irrefutable evidence washing hands after touching corpses and before delivering babies is a bad thing. Okay, hyperbolic a tad.
Brouwer inspired thinkers, and two of them were Heyting and Kolmogorov. In turn, they inspired Per Martin-Löf. His claim to fame is an intuitionist type theory (SEP). Think about that. Intuitionism rejects the notion that human minds are detached from deductivism, the classic fare of logical systems, and instead argues that logic systems are tools that harness psychological intuition; add to that a good type theory to avoid Russell's paradox, and you now have a radically different logical program from what Frege, Russell, and Tarski were working on. In fact, you might have the beginning of a formal theory pulling from multiple formal sciences that seeks to do mathematical reasoning like a human mind does. In his paper Truth of a Proposition, Evidence of a Judgement, Validity of a Proof, Martin-Löf goes on to reduce Heyting's, Kolmogorov's, and Gentzen's calculus to an isomorphism based on the premise that propositions are calls to the human mind to judge, not just truth conditions floating disembodied in a model-theoretic model. Incisively, he claims:
What is characteristic of this whole analysis, intuitionistic or verificationistic analysis, of the notions of proposition and truth is that the notion of proof of a proposition is conceptually prior (emphasis mine) to the notion of truth.
Whoa! He then goes on to trace this to Kant, talk about Bolzano, Brentano, and Husserl in much more detail. He then attempts to wrap up his excursion into historicity by arguing and drawing distinctions about realism and idealism, arguing essentially that appeals to correctness and the use of systems like Hoare's logic (not mentioned specifically), are grounded in the intuition of human judgement.
For computer scientists, any philosophical explication on correctness is extremely important because computer science, in the big picture, practices design (SEP), such as the design of languages, the design of specifications, and the design of computers. One of the primary questions in the process is, have I done it correctly? If you ever work as a software dev, you'll know that the constant baba yaga of coding is bugs. Bugs in the hardware, bugs in the EEPROM, bugs in the compiler, bugs in the code at compile-time and run-time, and bugs in other programmers' heads. Computer science myth literally tells of a moth stuck in a naval computer that Radm. Grace Hopper had to pluck from the circuits. (Also, see antipatterns for more information on an amusing canon of literature regarding the bugs generated by wetware.) Now, we are in a position to answer your question. To wit:
Can computer science be used to "test" theories of logic?
My dear sir, EVERY aspect of computer science is a test of theories of logic in one way or another. In intro discrete math courses, young computer scientists are taught that in 1854, George Boole in his book Laws of Thought essentially laid the golden egg for automatic computation by creating Boolean logic/algebra. The chapter that had that in my undergraduate education ended with using boolean algebra along side logic circuits check for correctness of design. So, computer scientists are obsessed with logics starting with the same fare that professional logicians are taught, and then diverging into their own domains. Algorithms, which are abstract maps to achieve goals are written in type-theoretic structures some of which, the functional sorts, are modeled on lambda calculus (which is equivalent to Turing's work). In fact, computer science in the modern sense began when Turing came to Princeton and along with other great mathematicians who invented computability theory (SEP), practiced mathematical logic. Kleene, Church, Turing? They were mathematical logicicans. I have a copy of Turing's thesis, and it's a logic. What makes computer science different from mathematical logic is not that mathematicians study logic and computer scientists study computers, no. It's that mathematicians run their mouths and produce fancy papers, but aren't constrained by the physical realities of having to build and operate computers that embody physical computation (SEP). (Platonic thinking is magical thinking when you have to build number systems from physical parts.) Traditionally, mathematicians play with abstract objects, and physicists build apparatuses to test physical objects; a computer scientist must master both domains. (Oversimplification, of course. Mathematical physics is arguably more math than physics, and applied mathematicians very much care about the correctness of their models; and the best and brightest thinkers in their field always have their nose in adjacent territory.)
I could spend all day waxing on about the relationship between computers and math, but my advice is you to read Colburn's Philosophy and Computer Science and then move on. Not my favorite, but it's a good start.
Is this just... trivial, even? My intuition is telling me that non-deductive methods of reasoning in mathematics are somehow relevant to the viability of my question, and to the triviality (or nontriviality) of possible answers
Oh, deduction, induction, and abduction are all absolutely part of the core of correctness, be it correctness of programming language semantics or microcode design on a VLSI, multi-core processor. Computer scientists are designers, and at all levels, correct design is imperative. Russell's type theory (computer's don't handle contradiction well) is the basis of all programming language design. For computer scientists, programming language primitives are signed and unsigned integers, booleans, floating point values, and strings, and those are types. And the imperative and declarative statements that use them often perform type checking both a compile-time and run-time. But programming language primitives are compositional objects built from data primitives in an operational code at the processor level. And what is the heart of a CPU? The ALU! The arithmetic-logic unit. If someone had a magic wand to turn the imaginary into something real, waving a wand over a logic system would produce a computer.
Induction, plays a role bridging the divide between the mathematical and hardware aspects on a pragmatic level. No matter how clever the wit and intentions of designers of all-things-computers, ultimately, there's no theoretical way to prove that physical implementations are correct except with inductive logic. And that inductive logic is physical experimentation. Build it, run it, and check the results. And AI folk figured out after ramming their head against the wall for a few decades that AI algorithms have to be constructed with probabilistic and defeasible logics (SEP). In fact, SEP has an entire entry dedicated to logic and artificial intelligence (SEP). Those are core inductive methods. Anyway, the details on AI stuff can be viewed looking at the encyclopedia of a textbook that is Russell and Norvig's (GB). You poke around there, and you'll see that all the chapters are just applications of three topics: statistics, algebra, and logic (with the exception of the robotics stuff).
Can computers be used to test logic? The answer is a resounding yes in more ways than I have textbooks on computers.