The paper solves how to reform Aristotelian syllogisms (ASs) to make it compatible with classic logic, and further formally deduct them in logic programming languages. It asserts that there exist two challenging problems in Aristotelian categorical propositions (ACPs) among ASs. One is inconsistently to regard the particular quantifier as the existential quantifier meanwhile as the partial, another one is lacking a quantifier binding the second term. To overcome the two problems, new forms of categorical propositions (called expanded categorical propositions, ECPs) are introduced without semantic confusion in interpretations of the particular quantifier, and with the remedied second quantifier. Naturally, made up of ECPs, the forms of quantifier-expanded syllogisms (QESs) are constructed. To deduct QESs, a formal system, also a Turing machine, is designed to decide and symbolically generate valid conclusions. Thus, a semantics-consistent and form-intact system of QESs, with deductive rules based on mathematically computing models has been established.